Theorem u4lem6 768

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 47	. 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 764	. . . . . . . 8 (a ->4 (a ->4 b)) = ((a' ^ b') v b)
3	2	lan 77	. . . . . . 7 (a ^ (a ->4 (a ->4 b))) = (a ^ ((a' ^ b') v b))
4		coman1 185	. . . . . . . . . 10 (a' ^ b') C a'
5	4	comcom7 460	. . . . . . . . 9 (a' ^ b') C a
6		coman2 186	. . . . . . . . . 10 (a' ^ b') C b'
7	6	comcom7 460	. . . . . . . . 9 (a' ^ b') C b
8	5, 7	fh2 470	. . . . . . . 8 (a ^ ((a' ^ b') v b)) = ((a ^ (a' ^ b')) v (a ^ b))
9		ax-a2 31	. . . . . . . . 9 ((a ^ (a' ^ b')) v (a ^ b)) = ((a ^ b) v (a ^ (a' ^ b')))
10		ancom 74	. . . . . . . . . . . 12 ((a ^ a') ^ b') = (b' ^ (a ^ a'))
11		anass 76	. . . . . . . . . . . 12 ((a ^ a') ^ b') = (a ^ (a' ^ b'))
12		dff 101	. . . . . . . . . . . . . . 15 0 = (a ^ a')
13	12	ax-r1 35	. . . . . . . . . . . . . 14 (a ^ a') = 0
14	13	lan 77	. . . . . . . . . . . . 13 (b' ^ (a ^ a')) = (b' ^ 0)
15		an0 108	. . . . . . . . . . . . 13 (b' ^ 0) = 0
16	14, 15	ax-r2 36	. . . . . . . . . . . 12 (b' ^ (a ^ a')) = 0
17	10, 11, 16	3tr2 64	. . . . . . . . . . 11 (a ^ (a' ^ b')) = 0
18	17	lor 70	. . . . . . . . . 10 ((a ^ b) v (a ^ (a' ^ b'))) = ((a ^ b) v 0)
19		or0 102	. . . . . . . . . 10 ((a ^ b) v 0) = (a ^ b)
20	18, 19	ax-r2 36	. . . . . . . . 9 ((a ^ b) v (a ^ (a' ^ b'))) = (a ^ b)
21	9, 20	ax-r2 36	. . . . . . . 8 ((a ^ (a' ^ b')) v (a ^ b)) = (a ^ b)
22	8, 21	ax-r2 36	. . . . . . 7 (a ^ ((a' ^ b') v b)) = (a ^ b)
23	3, 22	ax-r2 36	. . . . . 6 (a ^ (a ->4 (a ->4 b))) = (a ^ b)
24	2	lan 77	. . . . . . 7 (a' ^ (a ->4 (a ->4 b))) = (a' ^ ((a' ^ b') v b))
25	4, 7	fh2 470	. . . . . . . 8 (a' ^ ((a' ^ b') v b)) = ((a' ^ (a' ^ b')) v (a' ^ b))
26		anass 76	. . . . . . . . . . 11 ((a' ^ a') ^ b') = (a' ^ (a' ^ b'))
27	26	ax-r1 35	. . . . . . . . . 10 (a' ^ (a' ^ b')) = ((a' ^ a') ^ b')
28		anidm 111	. . . . . . . . . . 11 (a' ^ a') = a'
29	28	ran 78	. . . . . . . . . 10 ((a' ^ a') ^ b') = (a' ^ b')
30	27, 29	ax-r2 36	. . . . . . . . 9 (a' ^ (a' ^ b')) = (a' ^ b')
31	30	ax-r5 38	. . . . . . . 8 ((a' ^ (a' ^ b')) v (a' ^ b)) = ((a' ^ b') v (a' ^ b))
32	25, 31	ax-r2 36	. . . . . . 7 (a' ^ ((a' ^ b') v b)) = ((a' ^ b') v (a' ^ b))
33	24, 32	ax-r2 36	. . . . . 6 (a' ^ (a ->4 (a ->4 b))) = ((a' ^ b') v (a' ^ b))
34	23, 33	2or 72	. . . . 5 ((a ^ (a ->4 (a ->4 b))) v (a' ^ (a ->4 (a ->4 b)))) = ((a ^ b) v ((a' ^ b') v (a' ^ b)))
35		id 59	. . . . 5 ((a ^ b) v ((a' ^ b') v (a' ^ b))) = ((a ^ b) v ((a' ^ b') v (a' ^ b)))
36	34, 35	ax-r2 36	. . . 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 70	. . . . . . 7 (a' v (a ->4 (a ->4 b))) = (a' v ((a' ^ b') v b))
38		or12 80	. . . . . . . 8 (a' v ((a' ^ b') v b)) = ((a' ^ b') v (a' v b))
39		comor1 461	. . . . . . . . . 10 (a' v b) C a'
40		comor2 462	. . . . . . . . . . 11 (a' v b) C b
41	40	comcom2 183	. . . . . . . . . 10 (a' v b) C b'
42	39, 41	fh3r 475	. . . . . . . . 9 ((a' ^ b') v (a' v b)) = ((a' v (a' v b)) ^ (b' v (a' v b)))
43		ax-a3 32	. . . . . . . . . . . . 13 ((a' v a') v b) = (a' v (a' v b))
44	43	ax-r1 35	. . . . . . . . . . . 12 (a' v (a' v b)) = ((a' v a') v b)
45		oridm 110	. . . . . . . . . . . . 13 (a' v a') = a'
46	45	ax-r5 38	. . . . . . . . . . . 12 ((a' v a') v b) = (a' v b)
47	44, 46	ax-r2 36	. . . . . . . . . . 11 (a' v (a' v b)) = (a' v b)
48		or12 80	. . . . . . . . . . . 12 (b' v (a' v b)) = (a' v (b' v b))
49		ax-a2 31	. . . . . . . . . . . . . . 15 (b' v b) = (b v b')
50		df-t 41	. . . . . . . . . . . . . . . 16 1 = (b v b')
51	50	ax-r1 35	. . . . . . . . . . . . . . 15 (b v b') = 1
52	49, 51	ax-r2 36	. . . . . . . . . . . . . 14 (b' v b) = 1
53	52	lor 70	. . . . . . . . . . . . 13 (a' v (b' v b)) = (a' v 1)
54		or1 104	. . . . . . . . . . . . 13 (a' v 1) = 1
55	53, 54	ax-r2 36	. . . . . . . . . . . 12 (a' v (b' v b)) = 1
56	48, 55	ax-r2 36	. . . . . . . . . . 11 (b' v (a' v b)) = 1
57	47, 56	2an 79	. . . . . . . . . 10 ((a' v (a' v b)) ^ (b' v (a' v b))) = ((a' v b) ^ 1)
58		an1 106	. . . . . . . . . 10 ((a' v b) ^ 1) = (a' v b)
59	57, 58	ax-r2 36	. . . . . . . . 9 ((a' v (a' v b)) ^ (b' v (a' v b))) = (a' v b)
60	42, 59	ax-r2 36	. . . . . . . 8 ((a' ^ b') v (a' v b)) = (a' v b)
61	38, 60	ax-r2 36	. . . . . . 7 (a' v ((a' ^ b') v b)) = (a' v b)
62	37, 61	ax-r2 36	. . . . . 6 (a' v (a ->4 (a ->4 b))) = (a' v b)
63		u4lem5n 766	. . . . . 6 (a ->4 (a ->4 b))' = ((a v b) ^ b')
64	62, 63	2an 79	. . . . 5 ((a' v (a ->4 (a ->4 b))) ^ (a ->4 (a ->4 b))') = ((a' v b) ^ ((a v b) ^ b'))
65		id 59	. . . . 5 ((a' v b) ^ ((a v b) ^ b')) = ((a' v b) ^ ((a v b) ^ b'))
66	64, 65	ax-r2 36	. . . 4 ((a' v (a ->4 (a ->4 b))) ^ (a ->4 (a ->4 b))') = ((a' v b) ^ ((a v b) ^ b'))
67	36, 66	2or 72	. . 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 460	. . . . . . 7 (a' v b) C a
69	68, 40	com2an 484	. . . . . 6 (a' v b) C (a ^ b)
70	39, 41	com2an 484	. . . . . . 7 (a' v b) C (a' ^ b')
71	39, 40	com2an 484	. . . . . . 7 (a' v b) C (a' ^ b)
72	70, 71	com2or 483	. . . . . 6 (a' v b) C ((a' ^ b') v (a' ^ b))
73	69, 72	com2or 483	. . . . 5 (a' v b) C ((a ^ b) v ((a' ^ b') v (a' ^ b)))
74	68, 40	com2or 483	. . . . . 6 (a' v b) C (a v b)
75	74, 41	com2an 484	. . . . 5 (a' v b) C ((a v b) ^ b')
76	73, 75	fh4 472	. . . 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 161	. . . . . . . . 9 (a ^ b) =< b
78		leor 159	. . . . . . . . 9 b =< (a' v b)
79	77, 78	letr 137	. . . . . . . 8 (a ^ b) =< (a' v b)
80		lea 160	. . . . . . . . . 10 (a' ^ b') =< a'
81		lea 160	. . . . . . . . . 10 (a' ^ b) =< a'
82	80, 81