Formal logic to prove $x+1 = 1 +x$

So i've been stuck on this problem for about an hour. I can't figure out how to do it, and help would be absolutely amazing. This is what's given:

$0 + 1 = 1$

$\forall x (x + 0 = x)$

$\forall x \forall y [x + (y+1)= (x+y)+1]$

$[0 + 1 = 1 + 0 \wedge \forall x(x + 1 = 1 + x \rightarrow (x+1)+1 = 1+(x+1)))] \rightarrow \forall x (x+1=1+x)$

And with these premises, I need to get $\forall x (x+1=1+x)$.

Help would be great. I keep getting closeish, only to find I'm actually doing it totally wrong.

-
Sometimes it's good to give yourself more than an hour! – Yuval Filmus Dec 2 '10 at 4:54

The last axiom is basically your induction statement: it says that if you can prove that $x+1 = 1+x$ for $x=0$, and you can prove that if it holds for $x$ then it holds for $x+1$, then you can conclude that the statement $x+1=1+x$ holds for all $x$. So you want to use your first and second axioms, as well as your third axiom, to show that the premises of the last axiom hold. That will give the conclusion you want.

-

Step 1: Prove 0+1=1+0

Apply premise #2 for x=1, and substitute into premise #1.

Step 2: Prove Ax [x+1=1+x -> x+1+1=1+(x+1)]

Suppose k+1=1+k (premise)

Apply premise #3 for x=1, y=k. Substitute from last premise. Apply symmetry of = to get k+1+1=1+(k+1).

Generalize. Apply premise #4 to get required result.

-

$0 + 1 = 1 \Longrightarrow (0 + 1) + (0 + 1) \Longrightarrow (0 + 1 + 1)$ (associativity axiom) $\Longrightarrow (1 + 1)$ (identity axiom)

Continue this for $x$ number of $1$'s.

-
Do you mean $x$ ones instead of $n$ ones? – apnorton Dec 21 '14 at 4:47