Theorem i3con 551

Description: Theorem for Kalmbach implication. (Contributed by NM, 9-Nov-1997.)

Assertion

Ref	Expression
i3con	((a →3 b) →3 ((a →3 b) →3 (b⊥ →3 a⊥ ))) = 1

Proof of Theorem i3con

Step	Hyp	Ref	Expression
1		ni32 502	. . . . 5 (a →3 b)⊥ = ((a ∪ b) ∩ ((a ∩ b⊥ ) ∪ (a⊥ ∩ (a ∪ b⊥ ))))
2		i3n1 249	. . . . 5 (b⊥ →3 a⊥ ) = (((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (b⊥ ∩ (b ∪ a⊥ )))
3	1, 2	2or 72	. . . 4 ((a →3 b)⊥ ∪ (b⊥ →3 a⊥ )) = (((a ∪ b) ∩ ((a ∩ b⊥ ) ∪ (a⊥ ∩ (a ∪ b⊥ )))) ∪ (((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (b⊥ ∩ (b ∪ a⊥ ))))
4		ax-a2 31	. . . . 5 (((a ∪ b) ∩ ((a ∩ b⊥ ) ∪ (a⊥ ∩ (a ∪ b⊥ )))) ∪ (((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (b⊥ ∩ (b ∪ a⊥ )))) = ((((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (b⊥ ∩ (b ∪ a⊥ ))) ∪ ((a ∪ b) ∩ ((a ∩ b⊥ ) ∪ (a⊥ ∩ (a ∪ b⊥ )))))
5		comor2 462	. . . . . . . . . 10 (a ∪ b) C b
6		comor1 461	. . . . . . . . . . 11 (a ∪ b) C a
7	6	comcom2 183	. . . . . . . . . 10 (a ∪ b) C a⊥
8	5, 7	com2an 484	. . . . . . . . 9 (a ∪ b) C (b ∩ a⊥ )
9	5, 6	com2an 484	. . . . . . . . 9 (a ∪ b) C (b ∩ a)
10	8, 9	com2or 483	. . . . . . . 8 (a ∪ b) C ((b ∩ a⊥ ) ∪ (b ∩ a))
11	5	comcom2 183	. . . . . . . . 9 (a ∪ b) C b⊥
12	5, 7	com2or 483	. . . . . . . . 9 (a ∪ b) C (b ∪ a⊥ )
13	11, 12	com2an 484	. . . . . . . 8 (a ∪ b) C (b⊥ ∩ (b ∪ a⊥ ))
14	10, 13	com2or 483	. . . . . . 7 (a ∪ b) C (((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (b⊥ ∩ (b ∪ a⊥ )))
15	6, 11	com2an 484	. . . . . . . 8 (a ∪ b) C (a ∩ b⊥ )
16	6, 11	com2or 483	. . . . . . . . 9 (a ∪ b) C (a ∪ b⊥ )
17	7, 16	com2an 484	. . . . . . . 8 (a ∪ b) C (a⊥ ∩ (a ∪ b⊥ ))
18	15, 17	com2or 483	. . . . . . 7 (a ∪ b) C ((a ∩ b⊥ ) ∪ (a⊥ ∩ (a ∪ b⊥ )))
19	14, 18	fh4 472	. . . . . 6 ((((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (b⊥ ∩ (b ∪ a⊥ ))) ∪ ((a ∪ b) ∩ ((a ∩ b⊥ ) ∪ (a⊥ ∩ (a ∪ b⊥ ))))) = (((((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (b⊥ ∩ (b ∪ a⊥ ))) ∪ (a ∪ b)) ∩ ((((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (b⊥ ∩ (b ∪ a⊥ ))) ∪ ((a ∩ b⊥ ) ∪ (a⊥ ∩ (a ∪ b⊥ )))))
20		ax-a3 32	. . . . . . . 8 ((((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (b⊥ ∩ (b ∪ a⊥ ))) ∪ (a ∪ b)) = (((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ ((b⊥ ∩ (b ∪ a⊥ )) ∪ (a ∪ b)))
21		or12 80	. . . . . . . . 9 (((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ ((b⊥ ∩ (b ∪ a⊥ )) ∪ (a ∪ b))) = ((b⊥ ∩ (b ∪ a⊥ )) ∪ (((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (a ∪ b)))
22		ax-a3 32	. . . . . . . . . . . 12 (((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (a ∪ b)) = ((b ∩ a⊥ ) ∪ ((b ∩ a) ∪ (a ∪ b)))
23		ancom 74	. . . . . . . . . . . . . . . . 17 (b ∩ a) = (a ∩ b)
24		lea 160	. . . . . . . . . . . . . . . . 17 (a ∩ b) ≤ a
25	23, 24	bltr 138	. . . . . . . . . . . . . . . 16 (b ∩ a) ≤ a
26		leo 158	. . . . . . . . . . . . . . . 16 a ≤ (a ∪ b)
27	25, 26	letr 137	. . . . . . . . . . . . . . 15 (b ∩ a) ≤ (a ∪ b)
28	27	df-le2 131	. . . . . . . . . . . . . 14 ((b ∩ a) ∪ (a ∪ b)) = (a ∪ b)
29	28	lor 70	. . . . . . . . . . . . 13 ((b ∩ a⊥ ) ∪ ((b ∩ a) ∪ (a ∪ b))) = ((b ∩ a⊥ ) ∪ (a ∪ b))
30		ax-a2 31	. . . . . . . . . . . . . 14 ((b ∩ a⊥ ) ∪ (a ∪ b)) = ((a ∪ b) ∪ (b ∩ a⊥ ))
31		ax-a3 32	. . . . . . . . . . . . . . 15 ((a ∪ b) ∪ (b ∩ a⊥ )) = (a ∪ (b ∪ (b ∩ a⊥ )))
32		orabs 120	. . . . . . . . . . . . . . . 16 (b ∪ (b ∩ a⊥ )) = b
33	32	lor 70	. . . . . . . . . . . . . . 15 (a ∪ (b ∪ (b ∩ a⊥ ))) = (a ∪ b)
34	31, 33	ax-r2 36	. . . . . . . . . . . . . 14 ((a ∪ b) ∪ (b ∩ a⊥ )) = (a ∪ b)
35	30, 34	ax-r2 36	. . . . . . . . . . . . 13 ((b ∩ a⊥ ) ∪ (a ∪ b)) = (a ∪ b)
36	29, 35	ax-r2 36	. . . . . . . . . . . 12 ((b ∩ a⊥ ) ∪ ((b ∩ a) ∪ (a ∪ b))) = (a ∪ b)
37	22, 36	ax-r2 36	. . . . . . . . . . 11 (((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (a ∪ b)) = (a ∪ b)
38	37	lor 70	. . . . . . . . . 10 ((b⊥ ∩ (b ∪ a⊥ )) ∪ (((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (a ∪ b))) = ((b⊥ ∩ (b ∪ a⊥ )) ∪ (a ∪ b))
39		ax-a2 31	. . . . . . . . . . 11 ((b⊥ ∩ (b ∪ a⊥ )) ∪ (a ∪ b)) = ((a ∪ b) ∪ (b⊥ ∩ (b ∪ a⊥ )))
40	5	comcom 453	. . . . . . . . . . . . . 14 b C (a ∪ b)
41	40	comcom3 454	. . . . . . . . . . . . 13 b⊥ C (a ∪ b)
42		comorr 184	. . . . . . . . . . . . . 14 b C (b ∪ a⊥ )
43	42	comcom3 454	. . . . . . . . . . . . 13 b⊥ C (b ∪ a⊥ )
44	41, 43	fh4 472	. . . . . . . . . . . 12 ((a ∪ b) ∪ (b⊥ ∩ (b ∪ a⊥ ))) = (((a ∪ b) ∪ b⊥ ) ∩ ((a ∪ b) ∪ (b ∪ a⊥ )))
45		ax-a3 32	. . . . . . . . . . . . . . 15 ((a ∪ b) ∪ b⊥ ) = (a ∪ (b ∪ b⊥ ))
46		df-t 41	. . . . . . . . . . . . . . . . . 18 1 = (b ∪ b⊥ )
47	46	ax-r1 35	. . . . . . . . . . . . . . . . 17 (b ∪ b⊥ ) = 1
48	47	lor 70	. . . . . . . . . . . . . . . 16 (a ∪ (b ∪ b⊥ )) = (a ∪ 1)
49		or1 104	. . . . . . . . . . . . . . . 16 (a ∪ 1) = 1
50	48, 49	ax-r2 36	. . . . . . . . . . . . . . 15 (a ∪ (b ∪ b⊥ )) = 1
51	45, 50	ax-r2 36	. . . . . . . . . . . . . 14 ((a ∪ b) ∪ b⊥ ) = 1
52		ax-a2 31	. . . . . . . . . . . . . . . 16 (a ∪ b) = (b ∪ a)
53	52	ax-r5 38	. . . . . . . . . . . . . . 15 ((a ∪ b) ∪ (b ∪ a⊥ )) = ((b ∪ a) ∪ (b ∪ a⊥ ))
54		or4 84	. . . . . . . . . . . . . . . 16 ((b ∪ a) ∪ (b ∪ a⊥ )) = ((b ∪ b) ∪ (a ∪ a⊥ ))
55		df-t 41	. . . . . . . . . . . . . . . . . . 19 1 = (a ∪ a⊥ )
56	55	ax-r1 35	. . . . . . . . . . . . . . . . . 18 (a ∪ a⊥ ) = 1
57	56	lor 70	. . . . . . . . . . . . . . . . 17 ((b ∪ b) ∪ (a ∪ a⊥ )) = ((b ∪ b) ∪ 1)
58		or1 104	. . . . . . . . . . . . . . . . 17 ((b ∪ b) ∪ 1) = 1
59	57, 58	ax-r2 36	. . . . . . . . . . . . . . . 16 ((b ∪ b) ∪ (a ∪ a⊥ )) = 1
60	54, 59	ax-r2 36	. . . . . . . . . . . . . . 15 ((b ∪ a) ∪ (b ∪ a⊥ )) = 1
61	53, 60	ax-r2 36	. . . . . . . . . . . . . 14 ((a ∪ b) ∪ (b ∪ a⊥ )) = 1
62	51, 61	2an 79	. . . . . . . . . . . . 13 (((a ∪ b) ∪ b⊥ ) ∩ ((a ∪ b) ∪ (b ∪ a⊥ ))) = (1 ∩ 1)
63		an1 106	. . . . . . . . . . . . 13 (1 ∩ 1) = 1
64	62, 63	ax-r2 36	. . . . . . . . . . . 12 (((a ∪ b) ∪ b⊥ ) ∩ ((a ∪ b) ∪ (b ∪ a⊥ ))) = 1
65	44, 64	ax-r2 36	. . . . . . . . . . 11 ((a ∪ b) ∪ (b⊥ ∩ (b ∪ a⊥ ))) = 1
66	39, 65	ax-r2 36	. . . . . . . . . 10 ((b⊥ ∩ (b ∪ a⊥ )) ∪ (a ∪ b)) = 1
67	38, 66	ax-r2 36	. . . . . . . . 9 ((b⊥ ∩ (b ∪ a⊥ )) ∪ (((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (a ∪ b))) = 1
68	21, 67	ax-r2 36	. . . . . . . 8 (((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ ((b⊥ ∩ (b ∪ a⊥ )) ∪ (a ∪ b))) = 1
69	20, 68	ax-r2 36	. . . . . . 7 ((((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (b⊥ ∩ (b ∪ a⊥ ))) ∪ (a ∪ b)) = 1
70		ax-a3 32	. . . . . . . 8 ((((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (b⊥ ∩ (b ∪ a⊥ ))) ∪ ((a ∩ b⊥ ) ∪ (a⊥ ∩ (a ∪ b⊥ )))) = (((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ ((b⊥ ∩ (b ∪ a⊥ )) ∪ ((a ∩ b⊥ ) ∪ (a⊥ ∩ (a ∪ b⊥ )))))
71		ax-a2 31	. . . . . . . . . . 11 ((b ∩ a⊥ ) ∪ (b ∩ a)) = ((b ∩ a) ∪ (b ∩ a⊥ ))
72		ancom 74	. . . . . . . . . . . 12 (b ∩ a⊥ ) = (a⊥ ∩ b)
73	72	lor 70	. . . . . . . . . . 11 ((b ∩ a) ∪ (b ∩ a⊥ )) = ((b ∩ a) ∪ (a⊥ ∩ b))
74	71, 73	ax-r2 36	. . . . . . . . . 10 ((b ∩ a⊥ ) ∪ (b ∩ a)) = ((b ∩ a) ∪ (a⊥ ∩ b))
75		ax-a3 32	. . . . . . . . . . . 12 (((b⊥ ∩ (b ∪ a⊥ )) ∪ (a ∩ b⊥ )) ∪ (a⊥ ∩ (a ∪ b⊥ ))) = ((b⊥ ∩ (b ∪ a⊥ )) ∪ ((a ∩ b⊥ ) ∪ (a⊥ ∩ (a ∪ b⊥ ))))
76	75	ax-r1 35	. . . . . . . . . . 11 ((b⊥ ∩ (b ∪ a⊥ )) ∪ ((a ∩ b⊥ ) ∪ (a⊥ ∩ (a ∪ b⊥ )))) = (((b⊥ ∩ (b ∪ a⊥ )) ∪ (a ∩ b⊥ )) ∪ (a⊥ ∩ (a ∪ b⊥ )))
77		ax-a2 31	. . . . . . . . . . . . 13 ((b⊥ ∩ (b ∪ a⊥ )) ∪ (a ∩ b⊥ )) = ((a ∩ b⊥ ) ∪ (b⊥ ∩ (b ∪ a⊥ )))
78		coman2 186	. . . . . . . . . . . . . . . 16 (a ∩ b⊥ ) C b⊥
79	78	comcom 453	. . . . . . . . . . . . . . 15 b⊥ C (a ∩ b⊥ )
80	79, 43	fh4 472	. . . . . . . . . . . . . 14 ((a ∩ b⊥ ) ∪ (b⊥ ∩ (b ∪ a⊥ ))) = (((a ∩ b⊥ ) ∪ b⊥ ) ∩ ((a ∩ b⊥ ) ∪ (b ∪ a⊥ )))
81		ax-a2 31	. . . . . . . . . . . . . . . . 17 ((a ∩ b⊥ ) ∪ b⊥ ) = (b⊥ ∪ (a ∩ b⊥ ))
82		ancom 74	. . . . . . . . . . . . . . . . . . 19 (a ∩ b⊥ ) = (b⊥ ∩ a)
83	82	lor 70	. . . . . . . . . . . . . . . . . 18 (b⊥ ∪ (a ∩ b⊥ )) = (b⊥ ∪ (b⊥ ∩ a))
84		orabs 120	. . . . . . . . . . . . . . . . . 18 (b⊥ ∪ (b⊥ ∩ a)) = b⊥
85	83, 84	ax-r2 36	. . . . . . . . . . . . . . . . 17 (b⊥ ∪ (a ∩ b⊥ )) = b⊥
86	81, 85	ax-r2 36	. . . . . . . . . . . . . . . 16 ((a ∩ b⊥ ) ∪ b⊥ ) = b⊥
87		ax-a2 31	. . . . . . . . . . . . . . . . . . 19 (b ∪ a⊥ ) = (a⊥ ∪ b)
88		anor1 88	. . . . . . . . . . . . . . . . . . . . 21 (a ∩ b⊥ ) = (a⊥ ∪ b)⊥
89	88	con2 67	. . . . . . . . . . . . . . . . . . . 20 (a ∩ b⊥ )⊥ = (a⊥ ∪ b)
90	89	ax-r1 35	. . . . . . . . . . . . . . . . . . 19 (a⊥ ∪ b) = (a ∩ b⊥ )⊥
91	87, 90	ax-r2 36	. . . . . . . . . . . . . . . . . 18 (b ∪ a⊥ ) = (a ∩ b⊥ )⊥
92	91	lor 70	. . . . . . . . . . . . . . . . 17 ((a ∩ b⊥ ) ∪ (b ∪ a⊥ )) = ((a ∩ b⊥ ) ∪ (a ∩ b⊥ )⊥ )
93		df-t 41	. . . . . . . . . . . . . . . . . 18 1 = ((a ∩ b⊥ ) ∪ (a ∩ b⊥ )⊥ )
94	93	ax-r1 35	. . . . . . . . . . . . . . . . 17 ((a ∩ b⊥ ) ∪ (a ∩ b⊥ )⊥ ) = 1
95	92, 94	ax-r2 36	. . . . . . . . . . . . . . . 16 ((a ∩ b⊥ ) ∪ (b ∪ a⊥ )) = 1
96	86, 95	2an 79	. . . . . . . . . . . . . . 15 (((a ∩ b⊥ ) ∪ b⊥ ) ∩ ((a ∩ b⊥ ) ∪ (b ∪ a⊥ ))) = (b⊥ ∩ 1)
97		an1 106	. . . . . . . . . . . . . . 15 (b⊥ ∩ 1) = b⊥
98	96, 97	ax-r2 36	. . . . . . . . . . . . . 14 (((a ∩ b⊥ ) ∪ b⊥ ) ∩ ((a ∩ b⊥ ) ∪ (b ∪ a⊥ ))) = b⊥
99	80, 98	ax-r2 36	. . . . . . . . . . . . 13 ((a ∩ b⊥ ) ∪ (b⊥ ∩ (b ∪ a⊥ ))) = b⊥
100	77, 99	ax-r2 36	. . . . . . . . . . . 12 ((b⊥ ∩ (b ∪ a⊥ )) ∪ (a ∩ b⊥ )) = b⊥
101	100	ax-r5 38	. . . . . . . . . . 11 (((b⊥ ∩ (b ∪ a⊥ )) ∪ (a ∩ b⊥ )) ∪ (a⊥ ∩ (a ∪ b⊥ ))) = (b⊥ ∪ (a⊥ ∩ (a ∪ b⊥ )))
102	76, 101	ax-r2 36	. . . . . . . . . 10 ((b⊥ ∩ (b ∪ a⊥ )) ∪ ((a ∩ b⊥ ) ∪ (a⊥ ∩ (a ∪ b⊥ )))) = (b⊥ ∪ (a⊥ ∩ (a ∪ b⊥ )))
103	74, 102	2or 72	. . . . . . . . 9 (((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ ((b⊥ ∩ (b ∪ a⊥ )) ∪ ((a ∩ b⊥ ) ∪ (a⊥ ∩ (a ∪ b⊥ ))))) = (((b ∩ a) ∪ (a⊥ ∩ b)) ∪ (b⊥ ∪ (a⊥ ∩ (a ∪ b⊥ ))))
104		or4 84	. . . . . . . . . 10 (((b ∩ a) ∪ (a⊥ ∩ b)) ∪ (b⊥ ∪ (a⊥ ∩ (a ∪ b⊥ )))) = (((b ∩ a) ∪ b⊥ ) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ (a ∪ b⊥ ))))
105		coman1 185	. . . . . . . . . . . . . . 15 (a⊥ ∩ b) C a⊥
106	105	comcom 453	. . . . . . . . . . . . . 14 a⊥ C (a⊥ ∩ b)
107		comorr 184	. . . . . . . . . . . . . . 15 a C (a ∪ b⊥ )
108	107	comcom3 454	. . . . . . . . . . . . . 14 a⊥ C (a ∪ b⊥ )
109	106, 108	fh4 472	. . . . . . . . . . . . 13 ((a⊥ ∩ b) ∪ (a⊥ ∩ (a ∪ b⊥ ))) = (((a⊥ ∩ b) ∪ a⊥ ) ∩ ((a⊥ ∩ b) ∪ (a ∪ b⊥ )))
110		ax-a2 31	. . . . . . . . . . . . . . . 16 ((a⊥ ∩ b) ∪ a⊥ ) = (a⊥ ∪ (a⊥ ∩ b))
111		orabs 120	. . . . . . . . . . . . . . . 16 (a⊥ ∪ (a⊥ ∩ b)) = a⊥
112	110, 111	ax-r2 36	. . . . . . . . . . . . . . 15 ((a⊥ ∩ b) ∪ a⊥ ) = a⊥
113		anor2 89	. . . . . . . . . . . . . . . . . . 19 (a⊥ ∩ b) = (a ∪ b⊥ )⊥
114	113	con2 67	. . . . . . . . . . . . . . . . . 18 (a⊥ ∩ b)⊥ = (a ∪ b⊥ )
115	114	ax-r1 35	. . . . . . . . . . . . . . . . 17 (a ∪ b⊥ ) = (a⊥ ∩ b)⊥
116	115	lor 70	. . . . . . . . . . . . . . . 16 ((a⊥ ∩ b) ∪ (a ∪ b⊥ )) = ((a⊥ ∩ b) ∪ (a⊥ ∩ b)⊥ )
117		df-t 41	. . . . . . . . . . . . . . . . 17 1 = ((a⊥ ∩ b) ∪ (a⊥ ∩ b)⊥ )
118	117	ax-r1 35	. . . . . . . . . . . . . . . 16 ((a⊥ ∩ b) ∪ (a⊥ ∩ b)⊥ ) = 1
119	116, 118	ax-r2 36	. . . . . . . . . . . . . . 15 ((a⊥ ∩ b) ∪ (a ∪ b⊥ )) = 1
120	112, 119	2an 79	. . . . . . . . . . . . . 14 (((a⊥ ∩ b) ∪ a⊥ ) ∩ ((a⊥ ∩ b) ∪ (a ∪ b⊥ ))) = (a⊥ ∩ 1)
121		an1 106	. . . . . . . . . . . . . 14 (a⊥ ∩ 1) = a⊥
122	120, 121	ax-r2 36	. . . . . . . . . . . . 13 (((a⊥ ∩ b) ∪ a⊥ ) ∩ ((a⊥ ∩ b) ∪ (a ∪ b⊥ ))) = a⊥
123	109, 122	ax-r2 36	. . . . . . . . . . . 12 ((a⊥ ∩ b) ∪ (a⊥ ∩ (a ∪ b⊥ ))) = a⊥
124	123	lor 70	. . . . . . . . . . 11 (((b ∩ a) ∪ b⊥ ) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ (a ∪ b⊥ )))) = (((b ∩ a) ∪ b⊥ ) ∪ a⊥ )
125		df-a 40	. . . . . . . . . . . . . . 15 (b ∩ a) = (b⊥ ∪ a⊥ )⊥
126	125	con2 67	. . . . . . . . . . . . . 14 (b ∩ a)⊥ = (b⊥ ∪ a⊥ )
127	126	ax-r1 35	. . . . . . . . . . . . 13 (b⊥ ∪ a⊥ ) = (b ∩ a)⊥
128	127	lor 70	. . . . . . . . . . . 12 ((b ∩ a) ∪ (b⊥ ∪ a⊥ )) = ((b ∩ a) ∪ (b ∩ a)⊥ )
129		ax-a3 32	. . . . . . . . . . . 12 (((b ∩ a) ∪ b⊥ ) ∪ a⊥ ) = ((b ∩ a) ∪ (b⊥ ∪ a⊥ ))
130		df-t 41	. . . . . . . . . . . 12 1 = ((b ∩ a) ∪ (b ∩ a)⊥ )
131	128, 129, 130	3tr1 63	. . . . . . . . . . 11 (((b ∩ a) ∪ b⊥ ) ∪ a⊥ ) = 1
132	124, 131	ax-r2 36	. . . . . . . . . 10 (((b ∩ a) ∪ b⊥ ) ∪ ((a⊥ ∩ b) ∪ (a⊥ ∩ (a ∪ b⊥ )))) = 1
133	104, 132	ax-r2 36	. . . . . . . . 9 (((b ∩ a) ∪ (a⊥ ∩ b)) ∪ (b⊥ ∪ (a⊥ ∩ (a ∪ b⊥ )))) = 1
134	103, 133	ax-r2 36	. . . . . . . 8 (((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ ((b⊥ ∩ (b ∪ a⊥ )) ∪ ((a ∩ b⊥ ) ∪ (a⊥ ∩ (a ∪ b⊥ ))))) = 1
135	70, 134	ax-r2 36	. . . . . . 7 ((((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (b⊥ ∩ (b ∪ a⊥ ))) ∪ ((a ∩ b⊥ ) ∪ (a⊥ ∩ (a ∪ b⊥ )))) = 1
136	69, 135	2an 79	. . . . . 6 (((((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (b⊥ ∩ (b ∪ a⊥ ))) ∪ (a ∪ b)) ∩ ((((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (b⊥ ∩ (b ∪ a⊥ ))) ∪ ((a ∩ b⊥ ) ∪ (a⊥ ∩ (a ∪ b⊥ ))))) = (1 ∩ 1)
137	19, 136	ax-r2 36	. . . . 5 ((((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (b⊥ ∩ (b ∪ a⊥ ))) ∪ ((a ∪ b) ∩ ((a ∩ b⊥ ) ∪ (a⊥ ∩ (a ∪ b⊥ ))))) = (1 ∩ 1)
138	4, 137	ax-r2 36	. . . 4 (((a ∪ b) ∩ ((a ∩ b⊥ ) ∪ (a⊥ ∩ (a ∪ b⊥ )))) ∪ (((b ∩ a⊥ ) ∪ (b ∩ a)) ∪ (b⊥ ∩ (b ∪ a⊥ )))) = (1 ∩ 1)
139	3, 138	ax-r2 36	. . 3 ((a →3 b)⊥ ∪ (b⊥ →3 a⊥ )) = (1 ∩ 1)
140	139, 63	ax-r2 36	. 2 ((a →3 b)⊥ ∪ (b⊥ →3 a⊥ )) = 1
141	140	i0i3 512	1 ((a →3 b) →3 ((a →3 b) →3 (b⊥ →3 a⊥ ))) = 1

This proof depends on syntax axioms:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8   →₃ wi3 14

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-i3 46  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is used by: (None)