Theorem u4lem6 768

Description: Lemma for unified implication study. (Contributed by NM, 26-Dec-1997.)

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))) ∪ (a⊥ ∩ (a →4 (a →4 b)))) ∪ ((a⊥ ∪ (a →4 (a →4 b))) ∩ (a →4 (a →4 b))⊥ ))
2		u4lem5 764	. . . . . . . 8 (a →4 (a →4 b)) = ((a⊥ ∩ b⊥ ) ∪ b)
3	2	lan 77	. . . . . . 7 (a ∩ (a →4 (a →4 b))) = (a ∩ ((a⊥ ∩ b⊥ ) ∪ 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⊥ ) ∪ b)) = ((a ∩ (a⊥ ∩ b⊥ )) ∪ (a ∩ b))
9		ax-a2 31	. . . . . . . . 9 ((a ∩ (a⊥ ∩ b⊥ )) ∪ (a ∩ b)) = ((a ∩ b) ∪ (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) ∪ (a ∩ (a⊥ ∩ b⊥ ))) = ((a ∩ b) ∪ 0)
19		or0 102	. . . . . . . . . 10 ((a ∩ b) ∪ 0) = (a ∩ b)
20	18, 19	ax-r2 36	. . . . . . . . 9 ((a ∩ b) ∪ (a ∩ (a⊥ ∩ b⊥ ))) = (a ∩ b)
21	9, 20	ax-r2 36	. . . . . . . 8 ((a ∩ (a⊥ ∩ b⊥ )) ∪ (a ∩ b)) = (a ∩ b)
22	8, 21	ax-r2 36	. . . . . . 7 (a ∩ ((a⊥ ∩ b⊥ ) ∪ 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⊥ ) ∪ b))
25	4, 7	fh2 470	. . . . . . . 8 (a⊥ ∩ ((a⊥ ∩ b⊥ ) ∪ b)) = ((a⊥ ∩ (a⊥ ∩ b⊥ )) ∪ (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⊥ )) ∪ (a⊥ ∩ b)) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))
32	25, 31	ax-r2 36	. . . . . . 7 (a⊥ ∩ ((a⊥ ∩ b⊥ ) ∪ b)) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))
33	24, 32	ax-r2 36	. . . . . 6 (a⊥ ∩ (a →4 (a →4 b))) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))
34	23, 33	2or 72	. . . . 5 ((a ∩ (a →4 (a →4 b))) ∪ (a⊥ ∩ (a →4 (a →4 b)))) = ((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b)))
35		id 59	. . . . 5 ((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) = ((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b)))
36	34, 35	ax-r2 36	. . . 4 ((a ∩ (a →4 (a →4 b))) ∪ (a⊥ ∩ (a →4 (a →4 b)))) = ((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b)))
37	2	lor 70	. . . . . . 7 (a⊥ ∪ (a →4 (a →4 b))) = (a⊥ ∪ ((a⊥ ∩ b⊥ ) ∪ b))
38		or12 80	. . . . . . . 8 (a⊥ ∪ ((a⊥ ∩ b⊥ ) ∪ b)) = ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∪ b))
39		comor1 461	. . . . . . . . . 10 (a⊥ ∪ b) C a⊥
40		comor2 462	. . . . . . . . . . 11 (a⊥ ∪ b) C b
41	40	comcom2 183	. . . . . . . . . 10 (a⊥ ∪ b) C b⊥
42	39, 41	fh3r 475	. . . . . . . . 9 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∪ b)) = ((a⊥ ∪ (a⊥ ∪ b)) ∩ (b⊥ ∪ (a⊥ ∪ b)))
43		ax-a3 32	. . . . . . . . . . . . 13 ((a⊥ ∪ a⊥ ) ∪ b) = (a⊥ ∪ (a⊥ ∪ b))
44	43	ax-r1 35	. . . . . . . . . . . 12 (a⊥ ∪ (a⊥ ∪ b)) = ((a⊥ ∪ a⊥ ) ∪ b)
45		oridm 110	. . . . . . . . . . . . 13 (a⊥ ∪ a⊥ ) = a⊥
46	45	ax-r5 38	. . . . . . . . . . . 12 ((a⊥ ∪ a⊥ ) ∪ b) = (a⊥ ∪ b)
47	44, 46	ax-r2 36	. . . . . . . . . . 11 (a⊥ ∪ (a⊥ ∪ b)) = (a⊥ ∪ b)
48		or12 80	. . . . . . . . . . . 12 (b⊥ ∪ (a⊥ ∪ b)) = (a⊥ ∪ (b⊥ ∪ b))
49		ax-a2 31	. . . . . . . . . . . . . . 15 (b⊥ ∪ b) = (b ∪ b⊥ )
50		df-t 41	. . . . . . . . . . . . . . . 16 1 = (b ∪ b⊥ )
51	50	ax-r1 35	. . . . . . . . . . . . . . 15 (b ∪ b⊥ ) = 1
52	49, 51	ax-r2 36	. . . . . . . . . . . . . 14 (b⊥ ∪ b) = 1
53	52	lor 70	. . . . . . . . . . . . 13 (a⊥ ∪ (b⊥ ∪ b)) = (a⊥ ∪ 1)
54		or1 104	. . . . . . . . . . . . 13 (a⊥ ∪ 1) = 1
55	53, 54	ax-r2 36	. . . . . . . . . . . 12 (a⊥ ∪ (b⊥ ∪ b)) = 1
56	48, 55	ax-r2 36	. . . . . . . . . . 11 (b⊥ ∪ (a⊥ ∪ b)) = 1
57	47, 56	2an 79	. . . . . . . . . 10 ((a⊥ ∪ (a⊥ ∪ b)) ∩ (b⊥ ∪ (a⊥ ∪ b))) = ((a⊥ ∪ b) ∩ 1)
58		an1 106	. . . . . . . . . 10 ((a⊥ ∪ b) ∩ 1) = (a⊥ ∪ b)
59	57, 58	ax-r2 36	. . . . . . . . 9 ((a⊥ ∪ (a⊥ ∪ b)) ∩ (b⊥ ∪ (a⊥ ∪ b))) = (a⊥ ∪ b)
60	42, 59	ax-r2 36	. . . . . . . 8 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∪ b)) = (a⊥ ∪ b)
61	38, 60	ax-r2 36	. . . . . . 7 (a⊥ ∪ ((a⊥ ∩ b⊥ ) ∪ b)) = (a⊥ ∪ b)
62	37, 61	ax-r2 36	. . . . . 6 (a⊥ ∪ (a →4 (a →4 b))) = (a⊥ ∪ b)
63		u4lem5n 766	. . . . . 6 (a →4 (a →4 b))⊥ = ((a ∪ b) ∩ b⊥ )
64	62, 63	2an 79	. . . . 5 ((a⊥ ∪ (a →4 (a →4 b))) ∩ (a →4 (a →4 b))⊥ ) = ((a⊥ ∪ b) ∩ ((a ∪ b) ∩ b⊥ ))
65		id 59	. . . . 5 ((a⊥ ∪ b) ∩ ((a ∪ b) ∩ b⊥ )) = ((a⊥ ∪ b) ∩ ((a ∪ b) ∩ b⊥ ))
66	64, 65	ax-r2 36	. . . 4 ((a⊥ ∪ (a →4 (a →4 b))) ∩ (a →4 (a →4 b))⊥ ) = ((a⊥ ∪ b) ∩ ((a ∪ b) ∩ b⊥ ))
67	36, 66	2or 72	. . 3 (((a ∩ (a →4 (a →4 b))) ∪ (a⊥ ∩ (a →4 (a →4 b)))) ∪ ((a⊥ ∪ (a →4 (a →4 b))) ∩ (a →4 (a →4 b))⊥ )) = (((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ ((a⊥ ∪ b) ∩ ((a ∪ b) ∩ b⊥ )))
68	39	comcom7 460	. . . . . . 7 (a⊥ ∪ b) C a
69	68, 40	com2an 484	. . . . . 6 (a⊥ ∪ b) C (a ∩ b)
70	39, 41	com2an 484	. . . . . . 7 (a⊥ ∪ b) C (a⊥ ∩ b⊥ )
71	39, 40	com2an 484	. . . . . . 7 (a⊥ ∪ b) C (a⊥ ∩ b)
72	70, 71	com2or 483	. . . . . 6 (a⊥ ∪ b) C ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))
73	69, 72	com2or 483	. . . . 5 (a⊥ ∪ b) C ((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b)))
74	68, 40	com2or 483	. . . . . 6 (a⊥ ∪ b) C (a ∪ b)
75	74, 41	com2an 484	. . . . 5 (a⊥ ∪ b) C ((a ∪ b) ∩ b⊥ )
76	73, 75	fh4 472	. . . 4 (((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ ((a⊥ ∪ b) ∩ ((a ∪ b) ∩ b⊥ ))) = ((((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ (a⊥ ∪ b)) ∩ (((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ ((a ∪ b) ∩ b⊥ )))
77		lear 161	. . . . . . . . 9 (a ∩ b) ≤ b
78		leor 159	. . . . . . . . 9 b ≤ (a⊥ ∪ b)
79	77, 78	letr 137	. . . . . . . 8 (a ∩ b) ≤ (a⊥ ∪ b)
80		lea 160	. . . . . . . . . 10 (a⊥ ∩ b⊥ ) ≤ a⊥
81		lea 160	. . . . . . . . . 10 (a⊥ ∩ b) ≤ a⊥
82	80, 81	lel2or 170	. . . . . . . . 9 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b)) ≤ a⊥
83		leo 158	. . . . . . . . 9 a⊥ ≤ (a⊥ ∪ b)
84	82, 83	letr 137	. . . . . . . 8 ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b)) ≤ (a⊥ ∪ b)
85	79, 84	lel2or 170	. . . . . . 7 ((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ≤ (a⊥ ∪ b)
86	85	df-le2 131	. . . . . 6 (((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ (a⊥ ∪ b)) = (a⊥ ∪ b)
87		comor1 461	. . . . . . . . . 10 (a ∪ b) C a
88		comor2 462	. . . . . . . . . 10 (a ∪ b) C b
89	87, 88	com2an 484	. . . . . . . . 9 (a ∪ b) C (a ∩ b)
90	87	comcom2 183	. . . . . . . . . . 11 (a ∪ b) C a⊥
91	88	comcom2 183	. . . . . . . . . . 11 (a ∪ b) C b⊥
92	90, 91	com2an 484	. . . . . . . . . 10 (a ∪ b) C (a⊥ ∩ b⊥ )
93	90, 88	com2an 484	. . . . . . . . . 10 (a ∪ b) C (a⊥ ∩ b)
94	92, 93	com2or 483	. . . . . . . . 9 (a ∪ b) C ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))
95	89, 94	com2or 483	. . . . . . . 8 (a ∪ b) C ((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b)))
96	95, 91	fh4 472	. . . . . . 7 (((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ ((a ∪ b) ∩ b⊥ )) = ((((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ (a ∪ b)) ∩ (((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ b⊥ ))
97		or32 82	. . . . . . . . . 10 (((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ (a ∪ b)) = (((a ∩ b) ∪ (a ∪ b)) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b)))
98		ax-a3 32	. . . . . . . . . . . . 13 (((a ∩ b) ∪ (a ∪ b)) ∪ (a⊥ ∩ b⊥ )) = ((a ∩ b) ∪ ((a ∪ b) ∪ (a⊥ ∩ b⊥ )))
99		anor3 90	. . . . . . . . . . . . . . . . 17 (a⊥ ∩ b⊥ ) = (a ∪ b)⊥
100	99	lor 70	. . . . . . . . . . . . . . . 16 ((a ∪ b) ∪ (a⊥ ∩ b⊥ )) = ((a ∪ b) ∪ (a ∪ b)⊥ )
101		df-t 41	. . . . . . . . . . . . . . . . 17 1 = ((a ∪ b) ∪ (a ∪ b)⊥ )
102	101	ax-r1 35	. . . . . . . . . . . . . . . 16 ((a ∪ b) ∪ (a ∪ b)⊥ ) = 1
103	100, 102	ax-r2 36	. . . . . . . . . . . . . . 15 ((a ∪ b) ∪ (a⊥ ∩ b⊥ )) = 1
104	103	lor 70	. . . . . . . . . . . . . 14 ((a ∩ b) ∪ ((a ∪ b) ∪ (a⊥ ∩ b⊥ ))) = ((a ∩ b) ∪ 1)
105		or1 104	. . . . . . . . . . . . . 14 ((a ∩ b) ∪ 1) = 1
106	104, 105	ax-r2 36	. . . . . . . . . . . . 13 ((a ∩ b) ∪ ((a ∪ b) ∪ (a⊥ ∩ b⊥ ))) = 1
107	98, 106	ax-r2 36	. . . . . . . . . . . 12 (((a ∩ b) ∪ (a ∪ b)) ∪ (a⊥ ∩ b⊥ )) = 1
108	107	ax-r5 38	. . . . . . . . . . 11 ((((a ∩ b) ∪ (a ∪ b)) ∪ (a⊥ ∩ b⊥ )) ∪ (a⊥ ∩ b)) = (1 ∪ (a⊥ ∩ b))
109		ax-a3 32	. . . . . . . . . . 11 ((((a ∩ b) ∪ (a ∪ b)) ∪ (a⊥ ∩ b⊥ )) ∪ (a⊥ ∩ b)) = (((a ∩ b) ∪ (a ∪ b)) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b)))
110		ax-a2 31	. . . . . . . . . . . 12 (1 ∪ (a⊥ ∩ b)) = ((a⊥ ∩ b) ∪ 1)
111		or1 104	. . . . . . . . . . . 12 ((a⊥ ∩ b) ∪ 1) = 1
112	110, 111	ax-r2 36	. . . . . . . . . . 11 (1 ∪ (a⊥ ∩ b)) = 1
113	108, 109, 112	3tr2 64	. . . . . . . . . 10 (((a ∩ b) ∪ (a ∪ b)) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) = 1
114	97, 113	ax-r2 36	. . . . . . . . 9 (((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ (a ∪ b)) = 1
115		or12 80	. . . . . . . . . . 11 ((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) = ((a⊥ ∩ b⊥ ) ∪ ((a ∩ b) ∪ (a⊥ ∩ b)))
116	115	ax-r5 38	. . . . . . . . . 10 (((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ b⊥ ) = (((a⊥ ∩ b⊥ ) ∪ ((a ∩ b) ∪ (a⊥ ∩ b))) ∪ b⊥ )
117		lear 161	. . . . . . . . . . . . 13 (a⊥ ∩ b⊥ ) ≤ b⊥
118	117	df-le2 131	. . . . . . . . . . . 12 ((a⊥ ∩ b⊥ ) ∪ b⊥ ) = b⊥
119	118	ax-r5 38	. . . . . . . . . . 11 (((a⊥ ∩ b⊥ ) ∪ b⊥ ) ∪ ((a ∩ b) ∪ (a⊥ ∩ b))) = (b⊥ ∪ ((a ∩ b) ∪ (a⊥ ∩ b)))
120		or32 82	. . . . . . . . . . 11 (((a⊥ ∩ b⊥ ) ∪ ((a ∩ b) ∪ (a⊥ ∩ b))) ∪ b⊥ ) = (((a⊥ ∩ b⊥ ) ∪ b⊥ ) ∪ ((a ∩ b) ∪ (a⊥ ∩ b)))
121		id 59	. . . . . . . . . . 11 (b⊥ ∪ ((a ∩ b) ∪ (a⊥ ∩ b))) = (b⊥ ∪ ((a ∩ b) ∪ (a⊥ ∩ b)))
122	119, 120, 121	3tr1 63	. . . . . . . . . 10 (((a⊥ ∩ b⊥ ) ∪ ((a ∩ b) ∪ (a⊥ ∩ b))) ∪ b⊥ ) = (b⊥ ∪ ((a ∩ b) ∪ (a⊥ ∩ b)))
123	116, 122	ax-r2 36	. . . . . . . . 9 (((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ b⊥ ) = (b⊥ ∪ ((a ∩ b) ∪ (a⊥ ∩ b)))
124	114, 123	2an 79	. . . . . . . 8 ((((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ (a ∪ b)) ∩ (((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ b⊥ )) = (1 ∩ (b⊥ ∪ ((a ∩ b) ∪ (a⊥ ∩ b))))
125		ancom 74	. . . . . . . . 9 (1 ∩ (b⊥ ∪ ((a ∩ b) ∪ (a⊥ ∩ b)))) = ((b⊥ ∪ ((a ∩ b) ∪ (a⊥ ∩ b))) ∩ 1)
126		an1 106	. . . . . . . . 9 ((b⊥ ∪ ((a ∩ b) ∪ (a⊥ ∩ b))) ∩ 1) = (b⊥ ∪ ((a ∩ b) ∪ (a⊥ ∩ b)))
127	125, 126	ax-r2 36	. . . . . . . 8 (1 ∩ (b⊥ ∪ ((a ∩ b) ∪ (a⊥ ∩ b)))) = (b⊥ ∪ ((a ∩ b) ∪ (a⊥ ∩ b)))
128	124, 127	ax-r2 36	. . . . . . 7 ((((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ (a ∪ b)) ∩ (((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ b⊥ )) = (b⊥ ∪ ((a ∩ b) ∪ (a⊥ ∩ b)))
129	96, 128	ax-r2 36	. . . . . 6 (((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ ((a ∪ b) ∩ b⊥ )) = (b⊥ ∪ ((a ∩ b) ∪ (a⊥ ∩ b)))
130	86, 129	2an 79	. . . . 5 ((((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ (a⊥ ∪ b)) ∩ (((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ ((a ∪ b) ∩ b⊥ ))) = ((a⊥ ∪ b) ∩ (b⊥ ∪ ((a ∩ b) ∪ (a⊥ ∩ b))))
131		comorr2 463	. . . . . . . 8 b C (a⊥ ∪ b)
132	131	comcom3 454	. . . . . . 7 b⊥ C (a⊥ ∪ b)
133		comanr2 465	. . . . . . . . 9 b C (a ∩ b)
134		comanr2 465	. . . . . . . . 9 b C (a⊥ ∩ b)
135	133, 134	com2or 483	. . . . . . . 8 b C ((a ∩ b) ∪ (a⊥ ∩ b))
136	135	comcom3 454	. . . . . . 7 b⊥ C ((a ∩ b) ∪ (a⊥ ∩ b))
137	132, 136	fh2 470	. . . . . 6 ((a⊥ ∪ b) ∩ (b⊥ ∪ ((a ∩ b) ∪ (a⊥ ∩ b)))) = (((a⊥ ∪ b) ∩ b⊥ ) ∪ ((a⊥ ∪ b) ∩ ((a ∩ b) ∪ (a⊥ ∩ b))))
138		ax-a2 31	. . . . . . 7 (((a⊥ ∪ b) ∩ b⊥ ) ∪ ((a ∩ b) ∪ (a⊥ ∩ b))) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b) ∩ b⊥ ))
139		ancom 74	. . . . . . . . 9 ((a⊥ ∪ b) ∩ ((a ∩ b) ∪ (a⊥ ∩ b))) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (a⊥ ∪ b))
140		lear 161	. . . . . . . . . . . 12 (a⊥ ∩ b) ≤ b
141	77, 140	lel2or 170	. . . . . . . . . . 11 ((a ∩ b) ∪ (a⊥ ∩ b)) ≤ b
142	141, 78	letr 137	. . . . . . . . . 10 ((a ∩ b) ∪ (a⊥ ∩ b)) ≤ (a⊥ ∪ b)
143	142	df2le2 136	. . . . . . . . 9 (((a ∩ b) ∪ (a⊥ ∩ b)) ∩ (a⊥ ∪ b)) = ((a ∩ b) ∪ (a⊥ ∩ b))
144	139, 143	ax-r2 36	. . . . . . . 8 ((a⊥ ∪ b) ∩ ((a ∩ b) ∪ (a⊥ ∩ b))) = ((a ∩ b) ∪ (a⊥ ∩ b))
145	144	lor 70	. . . . . . 7 (((a⊥ ∪ b) ∩ b⊥ ) ∪ ((a⊥ ∪ b) ∩ ((a ∩ b) ∪ (a⊥ ∩ b)))) = (((a⊥ ∪ b) ∩ b⊥ ) ∪ ((a ∩ b) ∪ (a⊥ ∩ b)))
146		df-i4 47	. . . . . . 7 (a →4 b) = (((a ∩ b) ∪ (a⊥ ∩ b)) ∪ ((a⊥ ∪ b) ∩ b⊥ ))
147	138, 145, 146	3tr1 63	. . . . . 6 (((a⊥ ∪ b) ∩ b⊥ ) ∪ ((a⊥ ∪ b) ∩ ((a ∩ b) ∪ (a⊥ ∩ b)))) = (a →4 b)
148	137, 147	ax-r2 36	. . . . 5 ((a⊥ ∪ b) ∩ (b⊥ ∪ ((a ∩ b) ∪ (a⊥ ∩ b)))) = (a →4 b)
149	130, 148	ax-r2 36	. . . 4 ((((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ (a⊥ ∪ b)) ∩ (((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ ((a ∪ b) ∩ b⊥ ))) = (a →4 b)
150	76, 149	ax-r2 36	. . 3 (((a ∩ b) ∪ ((a⊥ ∩ b⊥ ) ∪ (a⊥ ∩ b))) ∪ ((a⊥ ∪ b) ∩ ((a ∪ b) ∩ b⊥ ))) = (a →4 b)
151	67, 150	ax-r2 36	. 2 (((a ∩ (a →4 (a →4 b))) ∪ (a⊥ ∩ (a →4 (a →4 b)))) ∪ ((a⊥ ∪ (a →4 (a →4 b))) ∩ (a →4 (a →4 b))⊥ )) = (a →4 b)
152	1, 151	ax-r2 36	1 (a →4 (a →4 (a →4 b))) = (a →4 b)

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8  0wf 9   →₄ wi4 15

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439

This proof depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i4 47  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is used by: (None)