Theorem u4lem6 750

Description: Lemma for unified implication study.

Assertion

Ref	Expression
u4lem6	(a ->4 (a ->4 (a ->4 b))) = (a ->4 b)

Proof of Theorem u4lem6

Step	Hyp	Ref	Expression
1		df-i4 46	. 2 (a ->4 (a ->4 (a ->4 b))) = (((a ^ (a ->4 (a ->4 b))) v (a_|_ ^ (a ->4 (a ->4 b)))) v ((a_|_ v (a ->4 (a ->4 b))) ^ (a ->4 (a ->4 b))_|_))
2		u4lem5 746	. . . . . . . 8 (a ->4 (a ->4 b)) = ((a_|_ ^ b_|_) v b)
3	2	lan 70	. . . . . . 7 (a ^ (a ->4 (a ->4 b))) = (a ^ ((a_|_ ^ b_|_) v b))
4		coman1 177	. . . . . . . . . 10 (a_|_ ^ b_|_) C a_|_
5	4	comcom7 442	. . . . . . . . 9 (a_|_ ^ b_|_) C a
6		coman2 178	. . . . . . . . . 10 (a_|_ ^ b_|_) C b_|_
7	6	comcom7 442	. . . . . . . . 9 (a_|_ ^ b_|_) C b
8	5, 7	fh2 452	. . . . . . . 8 (a ^ ((a_|_ ^ b_|_) v b)) = ((a ^ (a_|_ ^ b_|_)) v (a ^ b))
9		ax-a2 30	. . . . . . . . 9 ((a ^ (a_|_ ^ b_|_)) v (a ^ b)) = ((a ^ b) v (a ^ (a_|_ ^ b_|_)))
10		ancom 68	. . . . . . . . . . . 12 ((a ^ a_|_) ^ b_|_) = (b_|_ ^ (a ^ a_|_))
11		anass 69	. . . . . . . . . . . 12 ((a ^ a_|_) ^ b_|_) = (a ^ (a_|_ ^ b_|_))
12		dff 93	. . . . . . . . . . . . . . 15 0 = (a ^ a_|_)
13	12	ax-r1 34	. . . . . . . . . . . . . 14 (a ^ a_|_) = 0
14	13	lan 70	. . . . . . . . . . . . 13 (b_|_ ^ (a ^ a_|_)) = (b_|_ ^ 0)
15		an0 100	. . . . . . . . . . . . 13 (b_|_ ^ 0) = 0
16	14, 15	ax-r2 35	. . . . . . . . . . . 12 (b_|_ ^ (a ^ a_|_)) = 0
17	10, 11, 16	3tr2 61	. . . . . . . . . . 11 (a ^ (a_|_ ^ b_|_)) = 0
18	17	lor 66	. . . . . . . . . 10 ((a ^ b) v (a ^ (a_|_ ^ b_|_))) = ((a ^ b) v 0)
19		or0 94	. . . . . . . . . 10 ((a ^ b) v 0) = (a ^ b)
20	18, 19	ax-r2 35	. . . . . . . . 9 ((a ^ b) v (a ^ (a_|_ ^ b_|_))) = (a ^ b)
21	9, 20	ax-r2 35	. . . . . . . 8 ((a ^ (a_|_ ^ b_|_)) v (a ^ b)) = (a ^ b)
22	8, 21	ax-r2 35	. . . . . . 7 (a ^ ((a_|_ ^ b_|_) v b)) = (a ^ b)
23	3, 22	ax-r2 35	. . . . . 6 (a ^ (a ->4 (a ->4 b))) = (a ^ b)
24	2	lan 70	. . . . . . 7 (a_|_ ^ (a ->4 (a ->4 b))) = (a_|_ ^ ((a_|_ ^ b_|_) v b))
25	4, 7	fh2 452	. . . . . . . 8 (a_|_ ^ ((a_|_ ^ b_|_) v b)) = ((a_|_ ^ (a_|_ ^ b_|_)) v (a_|_ ^ b))
26		anass 69	. . . . . . . . . . 11 ((a_|_ ^ a_|_) ^ b_|_) = (a_|_ ^ (a_|_ ^ b_|_))
27	26	ax-r1 34	. . . . . . . . . 10 (a_|_ ^ (a_|_ ^ b_|_)) = ((a_|_ ^ a_|_) ^ b_|_)
28		anidm 103	. . . . . . . . . . 11 (a_|_ ^ a_|_) = a_|_
29	28	ran 71	. . . . . . . . . 10 ((a_|_ ^ a_|_) ^ b_|_) = (a_|_ ^ b_|_)
30	27, 29	ax-r2 35	. . . . . . . . 9 (a_|_ ^ (a_|_ ^ b_|_)) = (a_|_ ^ b_|_)
31	30	ax-r5 37	. . . . . . . 8 ((a_|_ ^ (a_|_ ^ b_|_)) v (a_|_ ^ b)) = ((a_|_ ^ b_|_) v (a_|_ ^ b))
32	25, 31	ax-r2 35	. . . . . . 7 (a_|_ ^ ((a_|_ ^ b_|_) v b)) = ((a_|_ ^ b_|_) v (a_|_ ^ b))
33	24, 32	ax-r2 35	. . . . . 6 (a_|_ ^ (a ->4 (a ->4 b))) = ((a_|_ ^ b_|_) v (a_|_ ^ b))
34	23, 33	2or 67	. . . . 5 ((a ^ (a ->4 (a ->4 b))) v (a_|_ ^ (a ->4 (a ->4 b)))) = ((a ^ b) v ((a_|_ ^ b_|_) v (a_|_ ^ b)))
35		id 58	. . . . 5 ((a ^ b) v ((a_|_ ^ b_|_) v (a_|_ ^ b))) = ((a ^ b) v ((a_|_ ^ b_|_) v (a_|_ ^ b)))
36	34, 35	ax-r2 35	. . . 4 ((a ^ (a ->4 (a ->4 b))) v (a_|_ ^ (a ->4 (a ->4 b)))) = ((a ^ b) v ((a_|_ ^ b_|_) v (a_|_ ^ b)))
37	2	lor 66	. . . . . . 7 (a_|_ v (a ->4 (a ->4 b))) = (a_|_ v ((a_|_ ^ b_|_) v b))
38		or12 73	. . . . . . . 8 (a_|_ v ((a_|_ ^ b_|_) v b)) = ((a_|_ ^ b_|_) v (a_|_ v b))
39		comor1 443	. . . . . . . . . 10 (a_|_ v b) C a_|_
40		comor2 444	. . . . . . . . . . 11 (a_|_ v b) C b
41	40	comcom2 175	. . . . . . . . . 10 (a_|_ v b) C b_|_
42	39, 41	fh3r 457	. . . . . . . . 9 ((a_|_ ^ b_|_) v (a_|_ v b)) = ((a_|_ v (a_|_ v b)) ^ (b_|_ v (a_|_ v b)))
43		ax-a3 31	. . . . . . . . . . . . 13 ((a_|_ v a_|_) v b) = (a_|_ v (a_|_ v b))
44	43	ax-r1 34	. . . . . . . . . . . 12 (a_|_ v (a_|_ v b)) = ((a_|_ v a_|_) v b)
45		oridm 102	. . . . . . . . . . . . 13 (a_|_ v a_|_) = a_|_
46	45	ax-r5 37	. . . . . . . . . . . 12 ((a_|_ v a_|_) v b) = (a_|_ v b)
47	44, 46	ax-r2 35	. . . . . . . . . . 11 (a_|_ v (a_|_ v b)) = (a_|_ v b)
48		or12 73	. . . . . . . . . . . 12 (b_|_ v (a_|_ v b)) = (a_|_ v (b_|_ v b))
49		ax-a2 30	. . . . . . . . . . . . . . 15 (b_|_ v b) = (b v b_|_)
50		df-t 40	. . . . . . . . . . . . . . . 16 1 = (b v b_|_)
51	50	ax-r1 34	. . . . . . . . . . . . . . 15 (b v b_|_) = 1
52	49, 51	ax-r2 35	. . . . . . . . . . . . . 14 (b_|_ v b) = 1
53	52	lor 66	. . . . . . . . . . . . 13 (a_|_ v (b_|_ v b)) = (a_|_ v 1)
54		or1 96	. . . . . . . . . . . . 13 (a_|_ v 1) = 1
55	53, 54	ax-r2 35	. . . . . . . . . . . 12 (a_|_ v (b_|_ v b)) = 1
56	48, 55	ax-r2 35	. . . . . . . . . . 11 (b_|_ v (a_|_ v b)) = 1
57	47, 56	2an 72	. . . . . . . . . 10 ((a_|_ v (a_|_ v b)) ^ (b_|_ v (a_|_ v b))) = ((a_|_ v b) ^ 1)
58		an1 98	. . . . . . . . . 10 ((a_|_ v b) ^ 1) = (a_|_ v b)
59	57, 58	ax-r2 35	. . . . . . . . 9 ((a_|_ v (a_|_ v b)) ^ (b_|_ v (a_|_ v b))) = (a_|_ v b)
60	42, 59	ax-r2 35	. . . . . . . 8 ((a_|_ ^ b_|_) v (a_|_ v b)) = (a_|_ v b)
61	38, 60	ax-r2 35	. . . . . . 7 (a_|_ v ((a_|_ ^ b_|_) v b)) = (a_|_ v b)
62	37, 61	ax-r2 35	. . . . . 6 (a_|_ v (a ->4 (a ->4 b))) = (a_|_ v b)
63		u4lem5n 748	. . . . . 6 (a ->4 (a ->4 b))_|_ = ((a v b) ^ b_|_)
64	62, 63	2an 72	. . . . 5 ((a_|_ v (a ->4 (a ->4 b))) ^ (a ->4 (a ->4 b))_|_) = ((a_|_ v b) ^ ((a v b) ^ b_|_))
65		id 58	. . . . 5 ((a_|_ v b) ^ ((a v b) ^ b_|_)) = ((a_|_ v b) ^ ((a v b) ^ b_|_))
66	64, 65	ax-r2 35	. . . 4 ((a_|_ v (a ->4 (a ->4 b))) ^ (a ->4 (a ->4 b))_|_) = ((a_|_ v b) ^ ((a v b) ^ b_|_))
67	36, 66	2or 67	. . 3 (((a ^ (a ->4 (a ->4 b))) v (a_|_ ^ (a ->4 (a ->4 b)))) v ((a_|_ v (a ->4 (a ->4 b))) ^ (a ->4 (a ->4 b))_|_)) = (((a ^ b) v ((a_|_ ^ b_|_) v (a_|_ ^ b))) v ((a_|_ v b) ^ ((a v b) ^ b_|_)))
68	39	comcom7 442	. . . . . . 7 (a_|_ v b) C a
69	68, 40	com2an 466	. . . . . 6 (a_|_ v b) C (a ^ b)
70	39, 41	com2an 466	. . . . . . 7 (a_|_ v b) C (a_|_ ^ b_|_)
71	39, 40	com2an 466	. . . . . . 7 (a_|_ v b) C (a_|_ ^ b)
72	70, 71	com2or 465	. . . . . 6 (a_|_ v b) C ((a_|_ ^ b_|_) v (a_|_ ^ b))
73	69, 72	com2or 465	. . . . 5 (a_|_ v b) C ((a ^ b) v ((a_|_ ^ b_|_) v (a_|_ ^ b)))
74	68, 40	com2or 465	. . . . . 6 (a_|_ v b) C (a v b)
75	74, 41	com2an 466	. . . . 5 (a_|_ v b) C ((a v b) ^ b_|_)
76	73, 75	fh4 454	. . . 4 (((a ^ b) v ((a_|_ ^ b_|_) v (a_|_ ^ b))) v ((a_|_ v b) ^ ((a v b) ^ b_|_))) = ((((a ^ b) v ((a_|_ ^ b_|_) v (a_|_ ^ b))) v (a_|_ v b)) ^ (((a ^ b) v ((a_|_ ^ b_|_) v (a_|_ ^ b))) v ((a v b) ^ b_|_)))
77		lear 153	. . . . . . . . 9 (a ^ b) =< b
78		leor 151	. . . . . . . . 9 b =< (a_|_ v b)
79	77, 78	letr 129	. . . . . . . 8 (a ^ b) =< (a_|_ v b)
80		lea 152	. . . . . . . . . 10 (a_|_ ^ b_|_) =< a_|_
81		lea 152	. . . . . . . . . 10 (a_|_ ^ b) =< a_|_
82	80, 81	lel2or 162	. . . . . . . . 9 ((a_|_ ^ b_|_) v (a_|_ ^ b)) =< a_|_
83		leo 150	. . . . . . . . 9 a_|_ =< (a_|_ v b)
84	82, 83	letr 129	. . . . . . . 8 ((a_|_ ^ b_|_