Given the Peano axioms, yes. But most attempts at a formal axiomatization of mathematics don't start from Peano. (If you start from arithmetic, you may have difficulty proving set theory.) Frege started from Cantor's naive set theory, which blew up in his face. Russell and Whitehead[1][2] finally started from formal logic and some weird typed version of set theory that no one has ever explained to me and thus that I fear with superstitious dread. And that takes somewhere over 300 pages to get to "1+1=2", and the proof isn't actually completed until page 86 of volume 2 (according to Wikipedia).
Further, that the fact is trivially provable from Peano's axioms still doesn't mean the proof is meaningless.
Further, that the fact is trivially provable from Peano's axioms still doesn't mean the proof is meaningless.
[1] https://en.wikipedia.org/wiki/Principia_Mathematica
[2] http://www.storyofmathematics.com/20th_russell.html