Theorem i3con 533

Description: Theorem for Kalmbach implication.

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

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 9   →₃ wi3 15

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-i3 45  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org