Theorem addS1 ≪ | index | src | ≫ 

theorem addS1 (a b: nat): $ suc a + b = suc (a + b) $;
StepHypRefExpression
1 addeq2 
x = b -> suc a + x = suc a + b
2 addeq2 
x = b -> a + x = a + b
3 2 suceqd 
x = b -> suc (a + x) = suc (a + b)
4 1, 3 eqeqd 
x = b -> (suc a + x = suc (a + x) <-> suc a + b = suc (a + b))
5 addeq2 
x = 0 -> suc a + x = suc a + 0
6 addeq2 
x = 0 -> a + x = a + 0
7 6 suceqd 
x = 0 -> suc (a + x) = suc (a + 0)
8 5, 7 eqeqd 
x = 0 -> (suc a + x = suc (a + x) <-> suc a + 0 = suc (a + 0))
9 addeq2 
x = y -> suc a + x = suc a + y
10 addeq2 
x = y -> a + x = a + y
11 10 suceqd 
x = y -> suc (a + x) = suc (a + y)
12 9, 11 eqeqd 
x = y -> (suc a + x = suc (a + x) <-> suc a + y = suc (a + y))
13 addeq2 
x = suc y -> suc a + x = suc a + suc y
14 addeq2 
x = suc y -> a + x = a + suc y
15 14 suceqd 
x = suc y -> suc (a + x) = suc (a + suc y)
16 13, 15 eqeqd 
x = suc y -> (suc a + x = suc (a + x) <-> suc a + suc y = suc (a + suc y))
17 eqtr4 
suc a + 0 = suc a -> suc (a + 0) = suc a -> suc a + 0 = suc (a + 0)
18 add0 
suc a + 0 = suc a
19 17, 18 ax_mp 
suc (a + 0) = suc a -> suc a + 0 = suc (a + 0)
20 suceq 
a + 0 = a -> suc (a + 0) = suc a
21 add0 
a + 0 = a
22 20, 21 ax_mp 
suc (a + 0) = suc a
23 19, 22 ax_mp 
suc a + 0 = suc (a + 0)
24 addS 
suc a + suc y = suc (suc a + y)
25 addS 
a + suc y = suc (a + y)
26 id 
suc a + y = suc (a + y) -> suc a + y = suc (a + y)
27 25, 26 syl6eqr 
suc a + y = suc (a + y) -> suc a + y = a + suc y
28 27 suceqd 
suc a + y = suc (a + y) -> suc (suc a + y) = suc (a + suc y)
29 24, 28 syl5eq 
suc a + y = suc (a + y) -> suc a + suc y = suc (a + suc y)
30 4, 8, 12, 16, 23, 29 ind 
suc a + b = suc (a + b)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_peano (peano2, peano5, addeq, add0, addS)