Theorem addass ≪ | index | src | ≫ 

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

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)