Theorem appendass ≪ | index | src | ≫

theorem appendass (l1 l2 l3: nat): $ (l1 ++ l2) ++ l3 = l1 ++ l2 ++ l3 $;

Step	Hyp	Ref	Expression
1		id	_1 = l1 -> _1 = l1
2	1	appendeq1d	_1 = l1 -> _1 ++ l2 = l1 ++ l2
3	2	appendeq1d	_1 = l1 -> (_1 ++ l2) ++ l3 = (l1 ++ l2) ++ l3
4	1	appendeq1d	_1 = l1 -> _1 ++ l2 ++ l3 = l1 ++ l2 ++ l3
5	3, 4	eqeqd	_1 = l1 -> ((_1 ++ l2) ++ l3 = _1 ++ l2 ++ l3 <-> (l1 ++ l2) ++ l3 = l1 ++ l2 ++ l3)
6		id	_1 = 0 -> _1 = 0
7	6	appendeq1d	_1 = 0 -> _1 ++ l2 = 0 ++ l2
8	7	appendeq1d	_1 = 0 -> (_1 ++ l2) ++ l3 = (0 ++ l2) ++ l3
9	6	appendeq1d	_1 = 0 -> _1 ++ l2 ++ l3 = 0 ++ l2 ++ l3
10	8, 9	eqeqd	_1 = 0 -> ((_1 ++ l2) ++ l3 = _1 ++ l2 ++ l3 <-> (0 ++ l2) ++ l3 = 0 ++ l2 ++ l3)
11		id	_1 = a2 -> _1 = a2
12	11	appendeq1d	_1 = a2 -> _1 ++ l2 = a2 ++ l2
13	12	appendeq1d	_1 = a2 -> (_1 ++ l2) ++ l3 = (a2 ++ l2) ++ l3
14	11	appendeq1d	_1 = a2 -> _1 ++ l2 ++ l3 = a2 ++ l2 ++ l3
15	13, 14	eqeqd	_1 = a2 -> ((_1 ++ l2) ++ l3 = _1 ++ l2 ++ l3 <-> (a2 ++ l2) ++ l3 = a2 ++ l2 ++ l3)
16		id	_1 = a1 : a2 -> _1 = a1 : a2
17	16	appendeq1d	_1 = a1 : a2 -> _1 ++ l2 = a1 : a2 ++ l2
18	17	appendeq1d	_1 = a1 : a2 -> (_1 ++ l2) ++ l3 = (a1 : a2 ++ l2) ++ l3
19	16	appendeq1d	_1 = a1 : a2 -> _1 ++ l2 ++ l3 = a1 : a2 ++ l2 ++ l3
20	18, 19	eqeqd	_1 = a1 : a2 -> ((_1 ++ l2) ++ l3 = _1 ++ l2 ++ l3 <-> (a1 : a2 ++ l2) ++ l3 = a1 : a2 ++ l2 ++ l3)
21		eqtr4	(0 ++ l2) ++ l3 = l2 ++ l3 -> 0 ++ l2 ++ l3 = l2 ++ l3 -> (0 ++ l2) ++ l3 = 0 ++ l2 ++ l3
22		appendeq1	0 ++ l2 = l2 -> (0 ++ l2) ++ l3 = l2 ++ l3
23		append0	0 ++ l2 = l2
24	22, 23	ax_mp	(0 ++ l2) ++ l3 = l2 ++ l3
25	21, 24	ax_mp	0 ++ l2 ++ l3 = l2 ++ l3 -> (0 ++ l2) ++ l3 = 0 ++ l2 ++ l3
26		append0	0 ++ l2 ++ l3 = l2 ++ l3
27	25, 26	ax_mp	(0 ++ l2) ++ l3 = 0 ++ l2 ++ l3
28		appendeq1	a1 : a2 ++ l2 = a1 : (a2 ++ l2) -> (a1 : a2 ++ l2) ++ l3 = a1 : (a2 ++ l2) ++ l3
29		appendS	a1 : a2 ++ l2 = a1 : (a2 ++ l2)
30	28, 29	ax_mp	(a1 : a2 ++ l2) ++ l3 = a1 : (a2 ++ l2) ++ l3
31		appendS	a1 : (a2 ++ l2) ++ l3 = a1 : ((a2 ++ l2) ++ l3)
32		appendS	a1 : a2 ++ l2 ++ l3 = a1 : (a2 ++ l2 ++ l3)
33		conseq2	(a2 ++ l2) ++ l3 = a2 ++ l2 ++ l3 -> a1 : ((a2 ++ l2) ++ l3) = a1 : (a2 ++ l2 ++ l3)
34	32, 33	syl6eqr	(a2 ++ l2) ++ l3 = a2 ++ l2 ++ l3 -> a1 : ((a2 ++ l2) ++ l3) = a1 : a2 ++ l2 ++ l3
35	31, 34	syl5eq	(a2 ++ l2) ++ l3 = a2 ++ l2 ++ l3 -> a1 : (a2 ++ l2) ++ l3 = a1 : a2 ++ l2 ++ l3
36	30, 35	syl5eq	(a2 ++ l2) ++ l3 = a2 ++ l2 ++ l3 -> (a1 : a2 ++ l2) ++ l3 = a1 : a2 ++ l2 ++ l3
37	5, 10, 15, 20, 27, 36	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)