Theorem ska2 432

Description: Soundness theorem for Kalmbach's quantum propositional logic axiom KA2.

Assertion

Ref	Expression
ska2	((a ≡ b)⊥ ∪ ((b ≡ c)⊥ ∪ (a ≡ c))) = 1

Proof of Theorem ska2

Step	Hyp	Ref	Expression
1		dfnb 95	. . 3 (a ≡ b)⊥ = ((a ∪ b) ∩ (a⊥ ∪ b⊥ ))
2		dfnb 95	. . . 4 (b ≡ c)⊥ = ((b ∪ c) ∩ (b⊥ ∪ c⊥ ))
3		dfb 94	. . . 4 (a ≡ c) = ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))
4	2, 3	2or 72	. . 3 ((b ≡ c)⊥ ∪ (a ≡ c)) = (((b ∪ c) ∩ (b⊥ ∪ c⊥ )) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ )))
5	1, 4	2or 72	. 2 ((a ≡ b)⊥ ∪ ((b ≡ c)⊥ ∪ (a ≡ c))) = (((a ∪ b) ∩ (a⊥ ∪ b⊥ )) ∪ (((b ∪ c) ∩ (b⊥ ∪ c⊥ )) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))))
6		ax-a3 32	. . . 4 ((((a ∪ b) ∩ (a⊥ ∪ b⊥ )) ∪ ((b ∪ c) ∩ (b⊥ ∪ c⊥ ))) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))) = (((a ∪ b) ∩ (a⊥ ∪ b⊥ )) ∪ (((b ∪ c) ∩ (b⊥ ∪ c⊥ )) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))))
7	6	ax-r1 35	. . 3 (((a ∪ b) ∩ (a⊥ ∪ b⊥ )) ∪ (((b ∪ c) ∩ (b⊥ ∪ c⊥ )) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ )))) = ((((a ∪ b) ∩ (a⊥ ∪ b⊥ )) ∪ ((b ∪ c) ∩ (b⊥ ∪ c⊥ ))) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ )))
8		id 59	. . . 4 ((((a ∪ b) ∩ (a⊥ ∪ b⊥ )) ∪ ((b ∪ c) ∩ (b⊥ ∪ c⊥ ))) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))) = ((((a ∪ b) ∩ (a⊥ ∪ b⊥ )) ∪ ((b ∪ c) ∩ (b⊥ ∪ c⊥ ))) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ )))
9		le1 146	. . . . 5 ((((a ∪ b) ∩ (a⊥ ∪ b⊥ )) ∪ ((b ∪ c) ∩ (b⊥ ∪ c⊥ ))) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))) ≤ 1
10		ax-a2 31	. . . . . . . . . 10 ((((a ∪ b) ∩ a⊥ ) ∪ ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))) = (((a ∩ c) ∪ (a⊥ ∩ c⊥ )) ∪ (((a ∪ b) ∩ a⊥ ) ∪ ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))))
11		or12 80	. . . . . . . . . . 11 (((a ∩ c) ∪ (a⊥ ∩ c⊥ )) ∪ (((a ∪ b) ∩ a⊥ ) ∪ ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ )))) = (((a ∪ b) ∩ a⊥ ) ∪ (((a ∩ c) ∪ (a⊥ ∩ c⊥ )) ∪ ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))))
12		or12 80	. . . . . . . . . . . . 13 (((a ∪ b) ∩ a⊥ ) ∪ ((a ∩ c) ∪ (((a⊥ ∩ c⊥ ) ∪ b⊥ ) ∪ ((b ∪ c) ∩ c⊥ )))) = ((a ∩ c) ∪ (((a ∪ b) ∩ a⊥ ) ∪ (((a⊥ ∩ c⊥ ) ∪ b⊥ ) ∪ ((b ∪ c) ∩ c⊥ ))))
13		or12 80	. . . . . . . . . . . . . . . 16 (((a ∪ b) ∩ a⊥ ) ∪ (((a⊥ ∩ c⊥ ) ∪ b⊥ ) ∪ ((b ∪ c) ∩ c⊥ ))) = (((a⊥ ∩ c⊥ ) ∪ b⊥ ) ∪ (((a ∪ b) ∩ a⊥ ) ∪ ((b ∪ c) ∩ c⊥ )))
14		ax-a3 32	. . . . . . . . . . . . . . . . 17 (((a⊥ ∩ c⊥ ) ∪ b⊥ ) ∪ (((a ∪ b) ∩ a⊥ ) ∪ ((b ∪ c) ∩ c⊥ ))) = ((a⊥ ∩ c⊥ ) ∪ (b⊥ ∪ (((a ∪ b) ∩ a⊥ ) ∪ ((b ∪ c) ∩ c⊥ ))))
15		orordi 112	. . . . . . . . . . . . . . . . . 18 (b⊥ ∪ (((a ∪ b) ∩ a⊥ ) ∪ ((b ∪ c) ∩ c⊥ ))) = ((b⊥ ∪ ((a ∪ b) ∩ a⊥ )) ∪ (b⊥ ∪ ((b ∪ c) ∩ c⊥ )))
16	15	lor 70	. . . . . . . . . . . . . . . . 17 ((a⊥ ∩ c⊥ ) ∪ (b⊥ ∪ (((a ∪ b) ∩ a⊥ ) ∪ ((b ∪ c) ∩ c⊥ )))) = ((a⊥ ∩ c⊥ ) ∪ ((b⊥ ∪ ((a ∪ b) ∩ a⊥ )) ∪ (b⊥ ∪ ((b ∪ c) ∩ c⊥ ))))
17	14, 16	ax-r2 36	. . . . . . . . . . . . . . . 16 (((a⊥ ∩ c⊥ ) ∪ b⊥ ) ∪ (((a ∪ b) ∩ a⊥ ) ∪ ((b ∪ c) ∩ c⊥ ))) = ((a⊥ ∩ c⊥ ) ∪ ((b⊥ ∪ ((a ∪ b) ∩ a⊥ )) ∪ (b⊥ ∪ ((b ∪ c) ∩ c⊥ ))))
18	13, 17	ax-r2 36	. . . . . . . . . . . . . . 15 (((a ∪ b) ∩ a⊥ ) ∪ (((a⊥ ∩ c⊥ ) ∪ b⊥ ) ∪ ((b ∪ c) ∩ c⊥ ))) = ((a⊥ ∩ c⊥ ) ∪ ((b⊥ ∪ ((a ∪ b) ∩ a⊥ )) ∪ (b⊥ ∪ ((b ∪ c) ∩ c⊥ ))))
19	18	lor 70	. . . . . . . . . . . . . 14 ((a ∩ c) ∪ (((a ∪ b) ∩ a⊥ ) ∪ (((a⊥ ∩ c⊥ ) ∪ b⊥ ) ∪ ((b ∪ c) ∩ c⊥ )))) = ((a ∩ c) ∪ ((a⊥ ∩ c⊥ ) ∪ ((b⊥ ∪ ((a ∪ b) ∩ a⊥ )) ∪ (b⊥ ∪ ((b ∪ c) ∩ c⊥ )))))
20		or12 80	. . . . . . . . . . . . . . . 16 ((a ∩ c) ∪ ((a⊥ ∩ c⊥ ) ∪ ((b⊥ ∪ a⊥ ) ∪ (b⊥ ∪ c⊥ )))) = ((a⊥ ∩ c⊥ ) ∪ ((a ∩ c) ∪ ((b⊥ ∪ a⊥ ) ∪ (b⊥ ∪ c⊥ ))))
21		le1 146	. . . . . . . . . . . . . . . . 17 ((a⊥ ∩ c⊥ ) ∪ ((a ∩ c) ∪ ((b⊥ ∪ a⊥ ) ∪ (b⊥ ∪ c⊥ )))) ≤ 1
22		df-t 41	. . . . . . . . . . . . . . . . . . . 20 1 = ((a ∩ c) ∪ (a ∩ c)⊥ )
23		oran3 93	. . . . . . . . . . . . . . . . . . . . . 22 (a⊥ ∪ c⊥ ) = (a ∩ c)⊥
24	23	lor 70	. . . . . . . . . . . . . . . . . . . . 21 ((a ∩ c) ∪ (a⊥ ∪ c⊥ )) = ((a ∩ c) ∪ (a ∩ c)⊥ )
25	24	ax-r1 35	. . . . . . . . . . . . . . . . . . . 20 ((a ∩ c) ∪ (a ∩ c)⊥ ) = ((a ∩ c) ∪ (a⊥ ∪ c⊥ ))
26	22, 25	ax-r2 36	. . . . . . . . . . . . . . . . . . 19 1 = ((a ∩ c) ∪ (a⊥ ∪ c⊥ ))
27		leor 159	. . . . . . . . . . . . . . . . . . . . 21 a⊥ ≤ (b⊥ ∪ a⊥ )
28		leor 159	. . . . . . . . . . . . . . . . . . . . 21 c⊥ ≤ (b⊥ ∪ c⊥ )
29	27, 28	le2or 168	. . . . . . . . . . . . . . . . . . . 20 (a⊥ ∪ c⊥ ) ≤ ((b⊥ ∪ a⊥ ) ∪ (b⊥ ∪ c⊥ ))
30	29	lelor 166	. . . . . . . . . . . . . . . . . . 19 ((a ∩ c) ∪ (a⊥ ∪ c⊥ )) ≤ ((a ∩ c) ∪ ((b⊥ ∪ a⊥ ) ∪ (b⊥ ∪ c⊥ )))
31	26, 30	bltr 138	. . . . . . . . . . . . . . . . . 18 1 ≤ ((a ∩ c) ∪ ((b⊥ ∪ a⊥ ) ∪ (b⊥ ∪ c⊥ )))
32		leor 159	. . . . . . . . . . . . . . . . . 18 ((a ∩ c) ∪ ((b⊥ ∪ a⊥ ) ∪ (b⊥ ∪ c⊥ ))) ≤ ((a⊥ ∩ c⊥ ) ∪ ((a ∩ c) ∪ ((b⊥ ∪ a⊥ ) ∪ (b⊥ ∪ c⊥ ))))
33	31, 32	letr 137	. . . . . . . . . . . . . . . . 17 1 ≤ ((a⊥ ∩ c⊥ ) ∪ ((a ∩ c) ∪ ((b⊥ ∪ a⊥ ) ∪ (b⊥ ∪ c⊥ ))))
34	21, 33	lebi 145	. . . . . . . . . . . . . . . 16 ((a⊥ ∩ c⊥ ) ∪ ((a ∩ c) ∪ ((b⊥ ∪ a⊥ ) ∪ (b⊥ ∪ c⊥ )))) = 1
35	20, 34	ax-r2 36	. . . . . . . . . . . . . . 15 ((a ∩ c) ∪ ((a⊥ ∩ c⊥ ) ∪ ((b⊥ ∪ a⊥ ) ∪ (b⊥ ∪ c⊥ )))) = 1
36		wcomorr 412	. . . . . . . . . . . . . . . . . . . . . . 23 C (b, (b ∪ a)) = 1
37		ax-a2 31	. . . . . . . . . . . . . . . . . . . . . . . 24 (b ∪ a) = (a ∪ b)
38	37	bi1 118	. . . . . . . . . . . . . . . . . . . . . . 23 ((b ∪ a) ≡ (a ∪ b)) = 1
39	36, 38	wcbtr 411	. . . . . . . . . . . . . . . . . . . . . 22 C (b, (a ∪ b)) = 1
40	39	wcomcom 414	. . . . . . . . . . . . . . . . . . . . 21 C ((a ∪ b), b) = 1
41	40	wcomcom2 415	. . . . . . . . . . . . . . . . . . . 20 C ((a ∪ b), b⊥ ) = 1
42		wcomorr 412	. . . . . . . . . . . . . . . . . . . . . 22 C (a, (a ∪ b)) = 1
43	42	wcomcom 414	. . . . . . . . . . . . . . . . . . . . 21 C ((a ∪ b), a) = 1
44	43	wcomcom2 415	. . . . . . . . . . . . . . . . . . . 20 C ((a ∪ b), a⊥ ) = 1
45	41, 44	wfh4 426	. . . . . . . . . . . . . . . . . . 19 ((b⊥ ∪ ((a ∪ b) ∩ a⊥ )) ≡ ((b⊥ ∪ (a ∪ b)) ∩ (b⊥ ∪ a⊥ ))) = 1
46		or12 80	. . . . . . . . . . . . . . . . . . . . . . 23 (b⊥ ∪ (a ∪ b)) = (a ∪ (b⊥ ∪ b))
47		ax-a2 31	. . . . . . . . . . . . . . . . . . . . . . . . . 26 (b⊥ ∪ b) = (b ∪ b⊥ )
48		df-t 41	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 1 = (b ∪ b⊥ )
49	48	ax-r1 35	. . . . . . . . . . . . . . . . . . . . . . . . . 26 (b ∪ b⊥ ) = 1
50	47, 49	ax-r2 36	. . . . . . . . . . . . . . . . . . . . . . . . 25 (b⊥ ∪ b) = 1
51	50	lor 70	. . . . . . . . . . . . . . . . . . . . . . . 24 (a ∪ (b⊥ ∪ b)) = (a ∪ 1)
52		or1 104	. . . . . . . . . . . . . . . . . . . . . . . 24 (a ∪ 1) = 1
53	51, 52	ax-r2 36	. . . . . . . . . . . . . . . . . . . . . . 23 (a ∪ (b⊥ ∪ b)) = 1
54	46, 53	ax-r2 36	. . . . . . . . . . . . . . . . . . . . . 22 (b⊥ ∪ (a ∪ b)) = 1
55	54	ran 78	. . . . . . . . . . . . . . . . . . . . 21 ((b⊥ ∪ (a ∪ b)) ∩ (b⊥ ∪ a⊥ )) = (1 ∩ (b⊥ ∪ a⊥ ))
56		ancom 74	. . . . . . . . . . . . . . . . . . . . . 22 (1 ∩ (b⊥ ∪ a⊥ )) = ((b⊥ ∪ a⊥ ) ∩ 1)
57		an1 106	. . . . . . . . . . . . . . . . . . . . . 22 ((b⊥ ∪ a⊥ ) ∩ 1) = (b⊥ ∪ a⊥ )
58	56, 57	ax-r2 36	. . . . . . . . . . . . . . . . . . . . 21 (1 ∩ (b⊥ ∪ a⊥ )) = (b⊥ ∪ a⊥ )
59	55, 58	ax-r2 36	. . . . . . . . . . . . . . . . . . . 20 ((b⊥ ∪ (a ∪ b)) ∩ (b⊥ ∪ a⊥ )) = (b⊥ ∪ a⊥ )
60	59	bi1 118	. . . . . . . . . . . . . . . . . . 19 (((b⊥ ∪ (a ∪ b)) ∩ (b⊥ ∪ a⊥ )) ≡ (b⊥ ∪ a⊥ )) = 1
61	45, 60	wr2 371	. . . . . . . . . . . . . . . . . 18 ((b⊥ ∪ ((a ∪ b) ∩ a⊥ )) ≡ (b⊥ ∪ a⊥ )) = 1
62		wcomorr 412	. . . . . . . . . . . . . . . . . . . . . 22 C (b, (b ∪ c)) = 1
63	62	wcomcom 414	. . . . . . . . . . . . . . . . . . . . 21 C ((b ∪ c), b) = 1
64	63	wcomcom2 415	. . . . . . . . . . . . . . . . . . . 20 C ((b ∪ c), b⊥ ) = 1
65		wcomorr 412	. . . . . . . . . . . . . . . . . . . . . . 23 C (c, (c ∪ b)) = 1
66		ax-a2 31	. . . . . . . . . . . . . . . . . . . . . . . 24 (c ∪ b) = (b ∪ c)
67	66	bi1 118	. . . . . . . . . . . . . . . . . . . . . . 23 ((c ∪ b) ≡ (b ∪ c)) = 1
68	65, 67	wcbtr 411	. . . . . . . . . . . . . . . . . . . . . 22 C (c, (b ∪ c)) = 1
69	68	wcomcom 414	. . . . . . . . . . . . . . . . . . . . 21 C ((b ∪ c), c) = 1
70	69	wcomcom2 415	. . . . . . . . . . . . . . . . . . . 20 C ((b ∪ c), c⊥ ) = 1
71	64, 70	wfh4 426	. . . . . . . . . . . . . . . . . . 19 ((b⊥ ∪ ((b ∪ c) ∩ c⊥ )) ≡ ((b⊥ ∪ (b ∪ c)) ∩ (b⊥ ∪ c⊥ ))) = 1
72		ax-a2 31	. . . . . . . . . . . . . . . . . . . . . . 23 (b⊥ ∪ (b ∪ c)) = ((b ∪ c) ∪ b⊥ )
73		or32 82	. . . . . . . . . . . . . . . . . . . . . . . 24 ((b ∪ c) ∪ b⊥ ) = ((b ∪ b⊥ ) ∪ c)
74		ax-a2 31	. . . . . . . . . . . . . . . . . . . . . . . . 25 ((b ∪ b⊥ ) ∪ c) = (c ∪ (b ∪ b⊥ ))
75	49	lor 70	. . . . . . . . . . . . . . . . . . . . . . . . . 26 (c ∪ (b ∪ b⊥ )) = (c ∪ 1)
76		or1 104	. . . . . . . . . . . . . . . . . . . . . . . . . 26 (c ∪ 1) = 1
77	75, 76	ax-r2 36	. . . . . . . . . . . . . . . . . . . . . . . . 25 (c ∪ (b ∪ b⊥ )) = 1
78	74, 77	ax-r2 36	. . . . . . . . . . . . . . . . . . . . . . . 24 ((b ∪ b⊥ ) ∪ c) = 1
79	73, 78	ax-r2 36	. . . . . . . . . . . . . . . . . . . . . . 23 ((b ∪ c) ∪ b⊥ ) = 1
80	72, 79	ax-r2 36	. . . . . . . . . . . . . . . . . . . . . 22 (b⊥ ∪ (b ∪ c)) = 1
81	80	ran 78	. . . . . . . . . . . . . . . . . . . . 21 ((b⊥ ∪ (b ∪ c)) ∩ (b⊥ ∪ c⊥ )) = (1 ∩ (b⊥ ∪ c⊥ ))
82		ancom 74	. . . . . . . . . . . . . . . . . . . . . 22 (1 ∩ (b⊥ ∪ c⊥ )) = ((b⊥ ∪ c⊥ ) ∩ 1)
83		an1 106	. . . . . . . . . . . . . . . . . . . . . 22 ((b⊥ ∪ c⊥ ) ∩ 1) = (b⊥ ∪ c⊥ )
84	82, 83	ax-r2 36	. . . . . . . . . . . . . . . . . . . . 21 (1 ∩ (b⊥ ∪ c⊥ )) = (b⊥ ∪ c⊥ )
85	81, 84	ax-r2 36	. . . . . . . . . . . . . . . . . . . 20 ((b⊥ ∪ (b ∪ c)) ∩ (b⊥ ∪ c⊥ )) = (b⊥ ∪ c⊥ )
86	85	bi1 118	. . . . . . . . . . . . . . . . . . 19 (((b⊥ ∪ (b ∪ c)) ∩ (b⊥ ∪ c⊥ )) ≡ (b⊥ ∪ c⊥ )) = 1
87	71, 86	wr2 371	. . . . . . . . . . . . . . . . . 18 ((b⊥ ∪ ((b ∪ c) ∩ c⊥ )) ≡ (b⊥ ∪ c⊥ )) = 1
88	61, 87	w2or 372	. . . . . . . . . . . . . . . . 17 (((b⊥ ∪ ((a ∪ b) ∩ a⊥ )) ∪ (b⊥ ∪ ((b ∪ c) ∩ c⊥ ))) ≡ ((b⊥ ∪ a⊥ ) ∪ (b⊥ ∪ c⊥ ))) = 1
89	88	wlor 368	. . . . . . . . . . . . . . . 16 (((a⊥ ∩ c⊥ ) ∪ ((b⊥ ∪ ((a ∪ b) ∩ a⊥ )) ∪ (b⊥ ∪ ((b ∪ c) ∩ c⊥ )))) ≡ ((a⊥ ∩ c⊥ ) ∪ ((b⊥ ∪ a⊥ ) ∪ (b⊥ ∪ c⊥ )))) = 1
90	89	wlor 368	. . . . . . . . . . . . . . 15 (((a ∩ c) ∪ ((a⊥ ∩ c⊥ ) ∪ ((b⊥ ∪ ((a ∪ b) ∩ a⊥ )) ∪ (b⊥ ∪ ((b ∪ c) ∩ c⊥ ))))) ≡ ((a ∩ c) ∪ ((a⊥ ∩ c⊥ ) ∪ ((b⊥ ∪ a⊥ ) ∪ (b⊥ ∪ c⊥ ))))) = 1
91	35, 90	wwbmpr 206	. . . . . . . . . . . . . 14 ((a ∩ c) ∪ ((a⊥ ∩ c⊥ ) ∪ ((b⊥ ∪ ((a ∪ b) ∩ a⊥ )) ∪ (b⊥ ∪ ((b ∪ c) ∩ c⊥ ))))) = 1
92	19, 91	ax-r2 36	. . . . . . . . . . . . 13 ((a ∩ c) ∪ (((a ∪ b) ∩ a⊥ ) ∪ (((a⊥ ∩ c⊥ ) ∪ b⊥ ) ∪ ((b ∪ c) ∩ c⊥ )))) = 1
93	12, 92	ax-r2 36	. . . . . . . . . . . 12 (((a ∪ b) ∩ a⊥ ) ∪ ((a ∩ c) ∪ (((a⊥ ∩ c⊥ ) ∪ b⊥ ) ∪ ((b ∪ c) ∩ c⊥ )))) = 1
94		ax-a3 32	. . . . . . . . . . . . . . 15 (((a ∩ c) ∪ (a⊥ ∩ c⊥ )) ∪ ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))) = ((a ∩ c) ∪ ((a⊥ ∩ c⊥ ) ∪ ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))))
95	94	bi1 118	. . . . . . . . . . . . . 14 ((((a ∩ c) ∪ (a⊥ ∩ c⊥ )) ∪ ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))) ≡ ((a ∩ c) ∪ ((a⊥ ∩ c⊥ ) ∪ ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))))) = 1
96		ax-a3 32	. . . . . . . . . . . . . . . . . 18 (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ ((a ∪ b) ∪ (b ∪ c)))) ∪ ((b ∪ c) ∩ c⊥ )) = ((a⊥ ∩ c⊥ ) ∪ ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ )))
97	96	ax-r1 35	. . . . . . . . . . . . . . . . 17 ((a⊥ ∩ c⊥ ) ∪ ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))) = (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ ((a ∪ b) ∪ (b ∪ c)))) ∪ ((b ∪ c) ∩ c⊥ ))
98	97	bi1 118	. . . . . . . . . . . . . . . 16 (((a⊥ ∩ c⊥ ) ∪ ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))) ≡ (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ ((a ∪ b) ∪ (b ∪ c)))) ∪ ((b ∪ c) ∩ c⊥ ))) = 1
99		ancom 74	. . . . . . . . . . . . . . . . . . . 20 (b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) = (((a ∪ b) ∪ (b ∪ c)) ∩ b⊥ )
100	99	lor 70	. . . . . . . . . . . . . . . . . . 19 ((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ ((a ∪ b) ∪ (b ∪ c)))) = ((a⊥ ∩ c⊥ ) ∪ (((a ∪ b) ∪ (b ∪ c)) ∩ b⊥ ))
101	100	bi1 118	. . . . . . . . . . . . . . . . . 18 (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ ((a ∪ b) ∪ (b ∪ c)))) ≡ ((a⊥ ∩ c⊥ ) ∪ (((a ∪ b) ∪ (b ∪ c)) ∩ b⊥ ))) = 1
102		wcomorr 412	. . . . . . . . . . . . . . . . . . . . . . . 24 C ((a ∪ c), ((a ∪ c) ∪ b)) = 1
103		orordir 113	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a ∪ c) ∪ b) = ((a ∪ b) ∪ (c ∪ b))
104	66	lor 70	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ((a ∪ b) ∪ (c ∪ b)) = ((a ∪ b) ∪ (b ∪ c))
105	103, 104	ax-r2 36	. . . . . . . . . . . . . . . . . . . . . . . . 25 ((a ∪ c) ∪ b) = ((a ∪ b) ∪ (b ∪ c))
106	105	bi1 118	. . . . . . . . . . . . . . . . . . . . . . . 24 (((a ∪ c) ∪ b) ≡ ((a ∪ b) ∪ (b ∪ c))) = 1
107	102, 106	wcbtr 411	. . . . . . . . . . . . . . . . . . . . . . 23 C ((a ∪ c), ((a ∪ b) ∪ (b ∪ c))) = 1
108	107	wcomcom 414	. . . . . . . . . . . . . . . . . . . . . 22 C (((a ∪ b) ∪ (b ∪ c)), (a ∪ c)) = 1
109	108	wcomcom2 415	. . . . . . . . . . . . . . . . . . . . 21 C (((a ∪ b) ∪ (b ∪ c)), (a ∪ c)⊥ ) = 1
110		anor3 90	. . . . . . . . . . . . . . . . . . . . . . 23 (a⊥ ∩ c⊥ ) = (a ∪ c)⊥
111	110	ax-r1 35	. . . . . . . . . . . . . . . . . . . . . 22 (a ∪ c)⊥ = (a⊥ ∩ c⊥ )
112	111	bi1 118	. . . . . . . . . . . . . . . . . . . . 21 ((a ∪ c)⊥ ≡ (a⊥ ∩ c⊥ )) = 1
113	109, 112	wcbtr 411	. . . . . . . . . . . . . . . . . . . 20 C (((a ∪ b) ∪ (b ∪ c)), (a⊥ ∩ c⊥ )) = 1
114	39, 62	wcom2or 427	. . . . . . . . . . . . . . . . . . . . . 22 C (b, ((a ∪ b) ∪ (b ∪ c))) = 1
115	114	wcomcom 414	. . . . . . . . . . . . . . . . . . . . 21 C (((a ∪ b) ∪ (b ∪ c)), b) = 1
116	115	wcomcom2 415	. . . . . . . . . . . . . . . . . . . 20 C (((a ∪ b) ∪ (b ∪ c)), b⊥ ) = 1
117	113, 116	wfh4 426	. . . . . . . . . . . . . . . . . . 19 (((a⊥ ∩ c⊥ ) ∪ (((a ∪ b) ∪ (b ∪ c)) ∩ b⊥ )) ≡ (((a⊥ ∩ c⊥ ) ∪ ((a ∪ b) ∪ (b ∪ c))) ∩ ((a⊥ ∩ c⊥ ) ∪ b⊥ ))) = 1
118		le1 146	. . . . . . . . . . . . . . . . . . . . . . 23 ((a⊥ ∩ c⊥ ) ∪ ((a ∪ b) ∪ (b ∪ c))) ≤ 1
119		df-t 41	. . . . . . . . . . . . . . . . . . . . . . . . 25 1 = ((a⊥ ∩ c⊥ ) ∪ (a⊥ ∩ c⊥ )⊥ )
120		oran 87	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 (a ∪ c) = (a⊥ ∩ c⊥ )⊥
121	120	ax-r1 35	. . . . . . . . . . . . . . . . . . . . . . . . . 26 (a⊥ ∩ c⊥ )⊥ = (a ∪ c)
122	121	lor 70	. . . . . . . . . . . . . . . . . . . . . . . . 25 ((a⊥ ∩ c⊥ ) ∪ (a⊥ ∩ c⊥ )⊥ ) = ((a⊥ ∩ c⊥ ) ∪ (a ∪ c))
123	119, 122	ax-r2 36	. . . . . . . . . . . . . . . . . . . . . . . 24 1 = ((a⊥ ∩ c⊥ ) ∪ (a ∪ c))
124		leo 158	. . . . . . . . . . . . . . . . . . . . . . . . . 26 a ≤ (a ∪ b)
125		leor 159	. . . . . . . . . . . . . . . . . . . . . . . . . 26 c ≤ (b ∪ c)
126	124, 125	le2or 168	. . . . . . . . . . . . . . . . . . . . . . . . 25 (a ∪ c) ≤ ((a ∪ b) ∪ (b ∪ c))
127	126	lelor 166	. . . . . . . . . . . . . . . . . . . . . . . 24 ((a⊥ ∩ c⊥ ) ∪ (a ∪ c)) ≤ ((a⊥ ∩ c⊥ ) ∪ ((a ∪ b) ∪ (b ∪ c)))
128	123, 127	bltr 138	. . . . . . . . . . . . . . . . . . . . . . 23 1 ≤ ((a⊥ ∩ c⊥ ) ∪ ((a ∪ b) ∪ (b ∪ c)))
129	118, 128	lebi 145	. . . . . . . . . . . . . . . . . . . . . 22 ((a⊥ ∩ c⊥ ) ∪ ((a ∪ b) ∪ (b ∪ c))) = 1
130	129	ran 78	. . . . . . . . . . . . . . . . . . . . 21 (((a⊥ ∩ c⊥ ) ∪ ((a ∪ b) ∪ (b ∪ c))) ∩ ((a⊥ ∩ c⊥ ) ∪ b⊥ )) = (1 ∩ ((a⊥ ∩ c⊥ ) ∪ b⊥ ))
131		ancom 74	. . . . . . . . . . . . . . . . . . . . . 22 (1 ∩ ((a⊥ ∩ c⊥ ) ∪ b⊥ )) = (((a⊥ ∩ c⊥ ) ∪ b⊥ ) ∩ 1)
132		an1 106	. . . . . . . . . . . . . . . . . . . . . 22 (((a⊥ ∩ c⊥ ) ∪ b⊥ ) ∩ 1) = ((a⊥ ∩ c⊥ ) ∪ b⊥ )
133	131, 132	ax-r2 36	. . . . . . . . . . . . . . . . . . . . 21 (1 ∩ ((a⊥ ∩ c⊥ ) ∪ b⊥ )) = ((a⊥ ∩ c⊥ ) ∪ b⊥ )
134	130, 133	ax-r2 36	. . . . . . . . . . . . . . . . . . . 20 (((a⊥ ∩ c⊥ ) ∪ ((a ∪ b) ∪ (b ∪ c))) ∩ ((a⊥ ∩ c⊥ ) ∪ b⊥ )) = ((a⊥ ∩ c⊥ ) ∪ b⊥ )
135	134	bi1 118	. . . . . . . . . . . . . . . . . . 19 ((((a⊥ ∩ c⊥ ) ∪ ((a ∪ b) ∪ (b ∪ c))) ∩ ((a⊥ ∩ c⊥ ) ∪ b⊥ )) ≡ ((a⊥ ∩ c⊥ ) ∪ b⊥ )) = 1
136	117, 135	wr2 371	. . . . . . . . . . . . . . . . . 18 (((a⊥ ∩ c⊥ ) ∪ (((a ∪ b) ∪ (b ∪ c)) ∩ b⊥ )) ≡ ((a⊥ ∩ c⊥ ) ∪ b⊥ )) = 1
137	101, 136	wr2 371	. . . . . . . . . . . . . . . . 17 (((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ ((a ∪ b) ∪ (b ∪ c)))) ≡ ((a⊥ ∩ c⊥ ) ∪ b⊥ )) = 1
138	137	wr5-2v 366	. . . . . . . . . . . . . . . 16 ((((a⊥ ∩ c⊥ ) ∪ (b⊥ ∩ ((a ∪ b) ∪ (b ∪ c)))) ∪ ((b ∪ c) ∩ c⊥ )) ≡ (((a⊥ ∩ c⊥ ) ∪ b⊥ ) ∪ ((b ∪ c) ∩ c⊥ ))) = 1
139	98, 138	wr2 371	. . . . . . . . . . . . . . 15 (((a⊥ ∩ c⊥ ) ∪ ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))) ≡ (((a⊥ ∩ c⊥ ) ∪ b⊥ ) ∪ ((b ∪ c) ∩ c⊥ ))) = 1
140	139	wlor 368	. . . . . . . . . . . . . 14 (((a ∩ c) ∪ ((a⊥ ∩ c⊥ ) ∪ ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ )))) ≡ ((a ∩ c) ∪ (((a⊥ ∩ c⊥ ) ∪ b⊥ ) ∪ ((b ∪ c) ∩ c⊥ )))) = 1
141	95, 140	wr2 371	. . . . . . . . . . . . 13 ((((a ∩ c) ∪ (a⊥ ∩ c⊥ )) ∪ ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))) ≡ ((a ∩ c) ∪ (((a⊥ ∩ c⊥ ) ∪ b⊥ ) ∪ ((b ∪ c) ∩ c⊥ )))) = 1
142	141	wlor 368	. . . . . . . . . . . 12 ((((a ∪ b) ∩ a⊥ ) ∪ (((a ∩ c) ∪ (a⊥ ∩ c⊥ )) ∪ ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ )))) ≡ (((a ∪ b) ∩ a⊥ ) ∪ ((a ∩ c) ∪ (((a⊥ ∩ c⊥ ) ∪ b⊥ ) ∪ ((b ∪ c) ∩ c⊥ ))))) = 1
143	93, 142	wwbmpr 206	. . . . . . . . . . 11 (((a ∪ b) ∩ a⊥ ) ∪ (((a ∩ c) ∪ (a⊥ ∩ c⊥ )) ∪ ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ )))) = 1
144	11, 143	ax-r2 36	. . . . . . . . . 10 (((a ∩ c) ∪ (a⊥ ∩ c⊥ )) ∪ (((a ∪ b) ∩ a⊥ ) ∪ ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ )))) = 1
145	10, 144	ax-r2 36	. . . . . . . . 9 ((((a ∪ b) ∩ a⊥ ) ∪ ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))) = 1
146	39	wcomcom3 416	. . . . . . . . . . . . 13 C (b⊥ , (a ∪ b)) = 1
147	62	wcomcom3 416	. . . . . . . . . . . . 13 C (b⊥ , (b ∪ c)) = 1
148	146, 147	wfh1 423	. . . . . . . . . . . 12 ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ≡ ((b⊥ ∩ (a ∪ b)) ∪ (b⊥ ∩ (b ∪ c)))) = 1
149	148	wr5-2v 366	. . . . . . . . . . 11 (((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ )) ≡ (((b⊥ ∩ (a ∪ b)) ∪ (b⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))) = 1
150	149	wlor 368	. . . . . . . . . 10 ((((a ∪ b) ∩ a⊥ ) ∪ ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))) ≡ (((a ∪ b) ∩ a⊥ ) ∪ (((b⊥ ∩ (a ∪ b)) ∪ (b⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ )))) = 1
151	150	wr5-2v 366	. . . . . . . . 9 (((((a ∪ b) ∩ a⊥ ) ∪ ((b⊥ ∩ ((a ∪ b) ∪ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))) ≡ ((((a ∪ b) ∩ a⊥ ) ∪ (((b⊥ ∩ (a ∪ b)) ∪ (b⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ )))) = 1
152	145, 151	wwbmp 205	. . . . . . . 8 ((((a ∪ b) ∩ a⊥ ) ∪ (((b⊥ ∩ (a ∪ b)) ∪ (b⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))) = 1
153	152	ax-r1 35	. . . . . . 7 1 = ((((a ∪ b) ∩ a⊥ ) ∪ (((b⊥ ∩ (a ∪ b)) ∪ (b⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ )))
154		ax-a3 32	. . . . . . . . . . 11 ((((a ∪ b) ∩ a⊥ ) ∪ ((b⊥ ∩ (a ∪ b)) ∪ (b⊥ ∩ (b ∪ c)))) ∪ ((b ∪ c) ∩ c⊥ )) = (((a ∪ b) ∩ a⊥ ) ∪ (((b⊥ ∩ (a ∪ b)) ∪ (b⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ )))
155	154	ax-r1 35	. . . . . . . . . 10 (((a ∪ b) ∩ a⊥ ) ∪ (((b⊥ ∩ (a ∪ b)) ∪ (b⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))) = ((((a ∪ b) ∩ a⊥ ) ∪ ((b⊥ ∩ (a ∪ b)) ∪ (b⊥ ∩ (b ∪ c)))) ∪ ((b ∪ c) ∩ c⊥ ))
156		ax-a3 32	. . . . . . . . . . . 12 ((((a ∪ b) ∩ a⊥ ) ∪ (b⊥ ∩ (a ∪ b))) ∪ (b⊥ ∩ (b ∪ c))) = (((a ∪ b) ∩ a⊥ ) ∪ ((b⊥ ∩ (a ∪ b)) ∪ (b⊥ ∩ (b ∪ c))))
157	156	ax-r1 35	. . . . . . . . . . 11 (((a ∪ b) ∩ a⊥ ) ∪ ((b⊥ ∩ (a ∪ b)) ∪ (b⊥ ∩ (b ∪ c)))) = ((((a ∪ b) ∩ a⊥ ) ∪ (b⊥ ∩ (a ∪ b))) ∪ (b⊥ ∩ (b ∪ c)))
158	157	ax-r5 38	. . . . . . . . . 10 ((((a ∪ b) ∩ a⊥ ) ∪ ((b⊥ ∩ (a ∪ b)) ∪ (b⊥ ∩ (b ∪ c)))) ∪ ((b ∪ c) ∩ c⊥ )) = (((((a ∪ b) ∩ a⊥ ) ∪ (b⊥ ∩ (a ∪ b))) ∪ (b⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))
159	155, 158	ax-r2 36	. . . . . . . . 9 (((a ∪ b) ∩ a⊥ ) ∪ (((b⊥ ∩ (a ∪ b)) ∪ (b⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))) = (((((a ∪ b) ∩ a⊥ ) ∪ (b⊥ ∩ (a ∪ b))) ∪ (b⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))
160		ax-a3 32	. . . . . . . . 9 (((((a ∪ b) ∩ a⊥ ) ∪ (b⊥ ∩ (a ∪ b))) ∪ (b⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ )) = ((((a ∪ b) ∩ a⊥ ) ∪ (b⊥ ∩ (a ∪ b))) ∪ ((b⊥ ∩ (b ∪ c)) ∪ ((b ∪ c) ∩ c⊥ )))
161	159, 160	ax-r2 36	. . . . . . . 8 (((a ∪ b) ∩ a⊥ ) ∪ (((b⊥ ∩ (a ∪ b)) ∪ (b⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))) = ((((a ∪ b) ∩ a⊥ ) ∪ (b⊥ ∩ (a ∪ b))) ∪ ((b⊥ ∩ (b ∪ c)) ∪ ((b ∪ c) ∩ c⊥ )))
162	161	ax-r5 38	. . . . . . 7 ((((a ∪ b) ∩ a⊥ ) ∪ (((b⊥ ∩ (a ∪ b)) ∪ (b⊥ ∩ (b ∪ c))) ∪ ((b ∪ c) ∩ c⊥ ))) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))) = (((((a ∪ b) ∩ a⊥ ) ∪ (b⊥ ∩ (a ∪ b))) ∪ ((b⊥ ∩ (b ∪ c)) ∪ ((b ∪ c) ∩ c⊥ ))) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ )))
163	153, 162	ax-r2 36	. . . . . 6 1 = (((((a ∪ b) ∩ a⊥ ) ∪ (b⊥ ∩ (a ∪ b))) ∪ ((b⊥ ∩ (b ∪ c)) ∪ ((b ∪ c) ∩ c⊥ ))) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ )))
164		ancom 74	. . . . . . . . . 10 (b⊥ ∩ (a ∪ b)) = ((a ∪ b) ∩ b⊥ )
165	164	lor 70	. . . . . . . . 9 (((a ∪ b) ∩ a⊥ ) ∪ (b⊥ ∩ (a ∪ b))) = (((a ∪ b) ∩ a⊥ ) ∪ ((a ∪ b) ∩ b⊥ ))
166		ledi 174	. . . . . . . . 9 (((a ∪ b) ∩ a⊥ ) ∪ ((a ∪ b) ∩ b⊥ )) ≤ ((a ∪ b) ∩ (a⊥ ∪ b⊥ ))
167	165, 166	bltr 138	. . . . . . . 8 (((a ∪ b) ∩ a⊥ ) ∪ (b⊥ ∩ (a ∪ b))) ≤ ((a ∪ b) ∩ (a⊥ ∪ b⊥ ))
168		ancom 74	. . . . . . . . . 10 (b⊥ ∩ (b ∪ c)) = ((b ∪ c) ∩ b⊥ )
169	168	ax-r5 38	. . . . . . . . 9 ((b⊥ ∩ (b ∪ c)) ∪ ((b ∪ c) ∩ c⊥ )) = (((b ∪ c) ∩ b⊥ ) ∪ ((b ∪ c) ∩ c⊥ ))
170		ledi 174	. . . . . . . . 9 (((b ∪ c) ∩ b⊥ ) ∪ ((b ∪ c) ∩ c⊥ )) ≤ ((b ∪ c) ∩ (b⊥ ∪ c⊥ ))
171	169, 170	bltr 138	. . . . . . . 8 ((b⊥ ∩ (b ∪ c)) ∪ ((b ∪ c) ∩ c⊥ )) ≤ ((b ∪ c) ∩ (b⊥ ∪ c⊥ ))
172	167, 171	le2or 168	. . . . . . 7 ((((a ∪ b) ∩ a⊥ ) ∪ (b⊥ ∩ (a ∪ b))) ∪ ((b⊥ ∩ (b ∪ c)) ∪ ((b ∪ c) ∩ c⊥ ))) ≤ (((a ∪ b) ∩ (a⊥ ∪ b⊥ )) ∪ ((b ∪ c) ∩ (b⊥ ∪ c⊥ )))
173	172	leror 152	. . . . . 6 (((((a ∪ b) ∩ a⊥ ) ∪ (b⊥ ∩ (a ∪ b))) ∪ ((b⊥ ∩ (b ∪ c)) ∪ ((b ∪ c) ∩ c⊥ ))) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))) ≤ ((((a ∪ b) ∩ (a⊥ ∪ b⊥ )) ∪ ((b ∪ c) ∩ (b⊥ ∪ c⊥ ))) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ )))
174	163, 173	bltr 138	. . . . 5 1 ≤ ((((a ∪ b) ∩ (a⊥ ∪ b⊥ )) ∪ ((b ∪ c) ∩ (b⊥ ∪ c⊥ ))) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ )))
175	9, 174	lebi 145	. . . 4 ((((a ∪ b) ∩ (a⊥ ∪ b⊥ )) ∪ ((b ∪ c) ∩ (b⊥ ∪ c⊥ ))) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))) = 1
176	8, 175	ax-r2 36	. . 3 ((((a ∪ b) ∩ (a⊥ ∪ b⊥ )) ∪ ((b ∪ c) ∩ (b⊥ ∪ c⊥ ))) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ ))) = 1
177	7, 176	ax-r2 36	. 2 (((a ∪ b) ∩ (a⊥ ∪ b⊥ )) ∪ (((b ∪ c) ∩ (b⊥ ∪ c⊥ )) ∪ ((a ∩ c) ∪ (a⊥ ∩ c⊥ )))) = 1
178	5, 177	ax-r2 36	1 ((a ≡ b)⊥ ∪ ((b ≡ c)⊥ ∪ (a ≡ c))) = 1

Syntax hints:   = wb 1  ^⊥ wn 4   ≡ tb 5   ∪ wo 6   ∩ wa 7  1wt 8

This theorem was proved from 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-wom 361

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-le 129  df-le1 130  df-le2 131  df-cmtr 134

This theorem is referenced by:  u3lemax5  797