Theorem appendass ≪ | index | src | ≫ 

theorem appendass (l1 l2 l3: nat): $ (l1 ++ l2) ++ l3 = l1 ++ l2 ++ l3 $;
StepHypRefExpression
1 id 
_1 = l1 -> _1 = l1
2 eqidd 
_1 = l1 -> l2 = l2
3 1, 2 appendeqd 
_1 = l1 -> _1 ++ l2 = l1 ++ l2
4 eqidd 
_1 = l1 -> l3 = l3
5 3, 4 appendeqd 
_1 = l1 -> (_1 ++ l2) ++ l3 = (l1 ++ l2) ++ l3
6 eqidd 
_1 = l1 -> l2 ++ l3 = l2 ++ l3
7 1, 6 appendeqd 
_1 = l1 -> _1 ++ l2 ++ l3 = l1 ++ l2 ++ l3
8 5, 7 eqeqd 
_1 = l1 -> ((_1 ++ l2) ++ l3 = _1 ++ l2 ++ l3 <-> (l1 ++ l2) ++ l3 = l1 ++ l2 ++ l3)
9 id 
_1 = 0 -> _1 = 0
10 eqidd 
_1 = 0 -> l2 = l2
11 9, 10 appendeqd 
_1 = 0 -> _1 ++ l2 = 0 ++ l2
12 eqidd 
_1 = 0 -> l3 = l3
13 11, 12 appendeqd 
_1 = 0 -> (_1 ++ l2) ++ l3 = (0 ++ l2) ++ l3
14 eqidd 
_1 = 0 -> l2 ++ l3 = l2 ++ l3
15 9, 14 appendeqd 
_1 = 0 -> _1 ++ l2 ++ l3 = 0 ++ l2 ++ l3
16 13, 15 eqeqd 
_1 = 0 -> ((_1 ++ l2) ++ l3 = _1 ++ l2 ++ l3 <-> (0 ++ l2) ++ l3 = 0 ++ l2 ++ l3)
17 id 
_1 = a2 -> _1 = a2
18 eqidd 
_1 = a2 -> l2 = l2
19 17, 18 appendeqd 
_1 = a2 -> _1 ++ l2 = a2 ++ l2
20 eqidd 
_1 = a2 -> l3 = l3
21 19, 20 appendeqd 
_1 = a2 -> (_1 ++ l2) ++ l3 = (a2 ++ l2) ++ l3
22 eqidd 
_1 = a2 -> l2 ++ l3 = l2 ++ l3
23 17, 22 appendeqd 
_1 = a2 -> _1 ++ l2 ++ l3 = a2 ++ l2 ++ l3
24 21, 23 eqeqd 
_1 = a2 -> ((_1 ++ l2) ++ l3 = _1 ++ l2 ++ l3 <-> (a2 ++ l2) ++ l3 = a2 ++ l2 ++ l3)
25 id 
_1 = a1 : a2 -> _1 = a1 : a2
26 eqidd 
_1 = a1 : a2 -> l2 = l2
27 25, 26 appendeqd 
_1 = a1 : a2 -> _1 ++ l2 = a1 : a2 ++ l2
28 eqidd 
_1 = a1 : a2 -> l3 = l3
29 27, 28 appendeqd 
_1 = a1 : a2 -> (_1 ++ l2) ++ l3 = (a1 : a2 ++ l2) ++ l3
30 eqidd 
_1 = a1 : a2 -> l2 ++ l3 = l2 ++ l3
31 25, 30 appendeqd 
_1 = a1 : a2 -> _1 ++ l2 ++ l3 = a1 : a2 ++ l2 ++ l3
32 29, 31 eqeqd 
_1 = a1 : a2 -> ((_1 ++ l2) ++ l3 = _1 ++ l2 ++ l3 <-> (a1 : a2 ++ l2) ++ l3 = a1 : a2 ++ l2 ++ l3)
33 eqtr4 
(0 ++ l2) ++ l3 = l2 ++ l3 -> 0 ++ l2 ++ l3 = l2 ++ l3 -> (0 ++ l2) ++ l3 = 0 ++ l2 ++ l3
34 appendeq1 
0 ++ l2 = l2 -> (0 ++ l2) ++ l3 = l2 ++ l3
35 append0 
0 ++ l2 = l2
36 34, 35 ax_mp 
(0 ++ l2) ++ l3 = l2 ++ l3
37 33, 36 ax_mp 
0 ++ l2 ++ l3 = l2 ++ l3 -> (0 ++ l2) ++ l3 = 0 ++ l2 ++ l3
38 append0 
0 ++ l2 ++ l3 = l2 ++ l3
39 37, 38 ax_mp 
(0 ++ l2) ++ l3 = 0 ++ l2 ++ l3
40 appendeq1 
a1 : a2 ++ l2 = a1 : (a2 ++ l2) -> (a1 : a2 ++ l2) ++ l3 = a1 : (a2 ++ l2) ++ l3
41 appendS 
a1 : a2 ++ l2 = a1 : (a2 ++ l2)
42 40, 41 ax_mp 
(a1 : a2 ++ l2) ++ l3 = a1 : (a2 ++ l2) ++ l3
43 appendS 
a1 : (a2 ++ l2) ++ l3 = a1 : ((a2 ++ l2) ++ l3)
44 appendS 
a1 : a2 ++ l2 ++ l3 = a1 : (a2 ++ l2 ++ l3)
45 conseq2 
(a2 ++ l2) ++ l3 = a2 ++ l2 ++ l3 -> a1 : ((a2 ++ l2) ++ l3) = a1 : (a2 ++ l2 ++ l3)
46 44, 45 syl6eqr 
(a2 ++ l2) ++ l3 = a2 ++ l2 ++ l3 -> a1 : ((a2 ++ l2) ++ l3) = a1 : a2 ++ l2 ++ l3
47 43, 46 syl5eq 
(a2 ++ l2) ++ l3 = a2 ++ l2 ++ l3 -> a1 : (a2 ++ l2) ++ l3 = a1 : a2 ++ l2 ++ l3
48 42, 47 syl5eq 
(a2 ++ l2) ++ l3 = a2 ++ l2 ++ l3 -> (a1 : a2 ++ l2) ++ l3 = a1 : a2 ++ l2 ++ l3
49 8, 16, 24, 32, 39, 48 listind 
(l1 ++ l2) ++ l3 = l1 ++ l2 ++ l3

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_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)