Theorem u1lem4 739

Description: Lemma for unified implication study.

Assertion

Ref	Expression
u1lem4	(a ->1 (a ->1 (b ->1 a))) = (a ->1 (b ->1 a))

Proof of Theorem u1lem4

Step	Hyp	Ref	Expression
1		df-i1 43	. 2 (a ->1 (a ->1 (b ->1 a))) = (a_|_ v (a ^ (a ->1 (b ->1 a))))
2		comid 179	. . . . 5 a C a
3	2	comcom2 175	. . . 4 a C a_|_
4		u1lemc1 662	. . . 4 a C (a ->1 (b ->1 a))
5	3, 4	fh4 454	. . 3 (a_|_ v (a ^ (a ->1 (b ->1 a)))) = ((a_|_ v a) ^ (a_|_ v (a ->1 (b ->1 a))))
6		ax-a2 30	. . . . . 6 (a_|_ v a) = (a v a_|_)
7		df-t 40	. . . . . . 7 1 = (a v a_|_)
8	7	ax-r1 34	. . . . . 6 (a v a_|_) = 1
9	6, 8	ax-r2 35	. . . . 5 (a_|_ v a) = 1
10		ax-a2 30	. . . . . 6 (a_|_ v (a ->1 (b ->1 a))) = ((a ->1 (b ->1 a)) v a_|_)
11		u1lemona 607	. . . . . . 7 ((a ->1 (b ->1 a)) v a_|_) = (a_|_ v (a ^ (b ->1 a)))
12		df-i1 43	. . . . . . . . . . 11 (b ->1 a) = (b_|_ v (b ^ a))
13		ancom 68	. . . . . . . . . . . 12 (b ^ a) = (a ^ b)
14	13	lor 66	. . . . . . . . . . 11 (b_|_ v (b ^ a)) = (b_|_ v (a ^ b))
15	12, 14	ax-r2 35	. . . . . . . . . 10 (b ->1 a) = (b_|_ v (a ^ b))
16	15	lan 70	. . . . . . . . 9 (a ^ (b ->1 a)) = (a ^ (b_|_ v (a ^ b)))
17	16	lor 66	. . . . . . . 8 (a_|_ v (a ^ (b ->1 a))) = (a_|_ v (a ^ (b_|_ v (a ^ b))))
18		u1lem3 731	. . . . . . . . . 10 (a ->1 (b ->1 a)) = (a_|_ v ((a ^ b) v (a ^ b_|_)))
19		ax-a2 30	. . . . . . . . . . . . . 14 (b_|_ v (a ^ b)) = ((a ^ b) v b_|_)
20	19	lan 70	. . . . . . . . . . . . 13 (a ^ (b_|_ v (a ^ b))) = (a ^ ((a ^ b) v b_|_))
21		coman1 177	. . . . . . . . . . . . . . 15 (a ^ b) C a
22		coman2 178	. . . . . . . . . . . . . . . 16 (a ^ b) C b
23	22	comcom2 175	. . . . . . . . . . . . . . 15 (a ^ b) C b_|_
24	21, 23	fh2 452	. . . . . . . . . . . . . 14 (a ^ ((a ^ b) v b_|_)) = ((a ^ (a ^ b)) v (a ^ b_|_))
25		anass 69	. . . . . . . . . . . . . . . . 17 ((a ^ a) ^ b) = (a ^ (a ^ b))
26	25	ax-r1 34	. . . . . . . . . . . . . . . 16 (a ^ (a ^ b)) = ((a ^ a) ^ b)
27		anidm 103	. . . . . . . . . . . . . . . . 17 (a ^ a) = a
28	27	ran 71	. . . . . . . . . . . . . . . 16 ((a ^ a) ^ b) = (a ^ b)
29	26, 28	ax-r2 35	. . . . . . . . . . . . . . 15 (a ^ (a ^ b)) = (a ^ b)
30	29	ax-r5 37	. . . . . . . . . . . . . 14 ((a ^ (a ^ b)) v (a ^ b_|_)) = ((a ^ b) v (a ^ b_|_))
31	24, 30	ax-r2 35	. . . . . . . . . . . . 13 (a ^ ((a ^ b) v b_|_)) = ((a ^ b) v (a ^ b_|_))
32	20, 31	ax-r2 35	. . . . . . . . . . . 12 (a ^ (b_|_ v (a ^ b))) = ((a ^ b) v (a ^ b_|_))
33	32	ax-r1 34	. . . . . . . . . . 11 ((a ^ b) v (a ^ b_|_)) = (a ^ (b_|_ v (a ^ b)))
34	33	lor 66	. . . . . . . . . 10 (a_|_ v ((a ^ b) v (a ^ b_|_))) = (a_|_ v (a ^ (b_|_ v (a ^ b))))
35	18, 34	ax-r2 35	. . . . . . . . 9 (a ->1 (b ->1 a)) = (a_|_ v (a ^ (b_|_ v (a ^ b))))
36	35	ax-r1 34	. . . . . . . 8 (a_|_ v (a ^ (b_|_ v (a ^ b)))) = (a ->1 (b ->1 a))
37	17, 36	ax-r2 35	. . . . . . 7 (a_|_ v (a ^ (b ->1 a))) = (a ->1 (b ->1 a))
38	11, 37	ax-r2 35	. . . . . 6 ((a ->1 (b ->1 a)) v a_|_) = (a ->1 (b ->1 a))
39	10, 38	ax-r2 35	. . . . 5 (a_|_ v (a ->1 (b ->1 a))) = (a ->1 (b ->1 a))
40	9, 39	2an 72	. . . 4 ((a_|_ v a) ^ (a_|_ v (a ->1 (b ->1 a)))) = (1 ^ (a ->1 (b ->1 a)))
41		ancom 68	. . . . 5 (1 ^ (a ->1 (b ->1 a))) = ((a ->1 (b ->1 a)) ^ 1)
42		an1 98	. . . . 5 ((a ->1 (b ->1 a)) ^ 1) = (a ->1 (b ->1 a))
43	41, 42	ax-r2 35	. . . 4 (1 ^ (a ->1 (b ->1 a))) = (a ->1 (b ->1 a))
44	40, 43	ax-r2 35	. . 3 ((a_|_ v a) ^ (a_|_ v (a ->1 (b ->1 a)))) = (a ->1 (b ->1 a))
45	5, 44	ax-r2 35	. 2 (a_|_ v (a ^ (a ->1 (b ->1 a)))) = (a ->1 (b ->1 a))
46	1, 45	ax-r2 35	1 (a ->1 (a ->1 (b ->1 a))) = (a ->1 (b ->1 a))

Syntax hints:   = wb 1  _|_wn 4   v wo 6   ^ wa 7  1wt 9   ->1 wi1 13

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a4 32  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-r3 421

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i1 43  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org