QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  oa4to4u GIF version
Theorem oa4to4u 973
Description: A "universal" 4-OA. The hypotheses are the standard proper 4-OA and substitutions into it. (Contributed by NM, 28-Dec-1998.)
Hypotheses
Ref Expression
oa4to4u.1 ((e →1 d) ∩ (e ∪ (f ∩ (((e ∩ f) ∪ ((e →1 d) ∩ (f →1 d))) ∪ (((e ∩ g) ∪ ((e →1 d) ∩ (g →1 d))) ∩ ((f ∩ g) ∪ ((f →1 d) ∩ (g →1 d)))))))) ≤ (((e ∩ d) ∪ (f ∩ d)) ∪ (g ∩ d))
oa4to4u.2 e = (a⊥ →1 d)
oa4to4u3 f = (b⊥ →1 d)
oa4to4u.4 g = (c⊥ →1 d)
Assertion
Ref Expression
oa4to4u ((a →1 d) ∩ ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a →1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) ∪ ((((a →1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b →1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d)))))))) ≤ ((((a →1 d) ∩ (a⊥ →1 d)) ∪ ((b →1 d) ∩ (b⊥ →1 d))) ∪ ((c →1 d) ∩ (c⊥ →1 d)))
Proof of Theorem oa4to4u
StepHypRef Expression
1 oa4to4u.1 . . 3 ((e →1 d) ∩ (e ∪ (f ∩ (((e ∩ f) ∪ ((e →1 d) ∩ (f →1 d))) ∪ (((e ∩ g) ∪ ((e →1 d) ∩ (g →1 d))) ∩ ((f ∩ g) ∪ ((f →1 d) ∩ (g →1 d)))))))) ≤ (((e ∩ d) ∪ (f ∩ d)) ∪ (g ∩ d))
2 oa4to4u.2 . . . . 5 e = (a⊥ →1 d)
32ud1lem0b 256 . . . 4 (e →1 d) = ((a⊥ →1 d) →1 d)
4 oa4to4u3 . . . . . 6 f = (b⊥ →1 d)
52, 42an 79 . . . . . . . 8 (e ∩ f) = ((a⊥ →1 d) ∩ (b⊥ →1 d))
64ud1lem0b 256 . . . . . . . . 9 (f →1 d) = ((b⊥ →1 d) →1 d)
73, 62an 79 . . . . . . . 8 ((e →1 d) ∩ (f →1 d)) = (((a⊥ →1 d) →1 d) ∩ ((b⊥ →1 d) →1 d))
85, 72or 72 . . . . . . 7 ((e ∩ f) ∪ ((e →1 d) ∩ (f →1 d))) = (((a⊥ →1 d) ∩ (b⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((b⊥ →1 d) →1 d)))
9 oa4to4u.4 . . . . . . . . . 10 g = (c⊥ →1 d)
102, 92an 79 . . . . . . . . 9 (e ∩ g) = ((a⊥ →1 d) ∩ (c⊥ →1 d))
119ud1lem0b 256 . . . . . . . . . 10 (g →1 d) = ((c⊥ →1 d) →1 d)
123, 112an 79 . . . . . . . . 9 ((e →1 d) ∩ (g →1 d)) = (((a⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))
1310, 122or 72 . . . . . . . 8 ((e ∩ g) ∪ ((e →1 d) ∩ (g →1 d))) = (((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d)))
144, 92an 79 . . . . . . . . 9 (f ∩ g) = ((b⊥ →1 d) ∩ (c⊥ →1 d))
156, 112an 79 . . . . . . . . 9 ((f →1 d) ∩ (g →1 d)) = (((b⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))
1614, 152or 72 . . . . . . . 8 ((f ∩ g) ∪ ((f →1 d) ∩ (g →1 d))) = (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((b⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d)))
1713, 162an 79 . . . . . . 7 (((e ∩ g) ∪ ((e →1 d) ∩ (g →1 d))) ∩ ((f ∩ g) ∪ ((f →1 d) ∩ (g →1 d)))) = ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((b⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))))
188, 172or 72 . . . . . 6 (((e ∩ f) ∪ ((e →1 d) ∩ (f →1 d))) ∪ (((e ∩ g) ∪ ((e →1 d) ∩ (g →1 d))) ∩ ((f ∩ g) ∪ ((f →1 d) ∩ (g →1 d))))) = ((((a⊥ →1 d) ∩ (b⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((b⊥ →1 d) →1 d))) ∪ ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((b⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d)))))
194, 182an 79 . . . . 5 (f ∩ (((e ∩ f) ∪ ((e →1 d) ∩ (f →1 d))) ∪ (((e ∩ g) ∪ ((e →1 d) ∩ (g →1 d))) ∩ ((f ∩ g) ∪ ((f →1 d) ∩ (g →1 d)))))) = ((b⊥ →1 d) ∩ ((((a⊥ →1 d) ∩ (b⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((b⊥ →1 d) →1 d))) ∪ ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((b⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))))))
202, 192or 72 . . . 4 (e ∪ (f ∩ (((e ∩ f) ∪ ((e →1 d) ∩ (f →1 d))) ∪ (((e ∩ g) ∪ ((e →1 d) ∩ (g →1 d))) ∩ ((f ∩ g) ∪ ((f →1 d) ∩ (g →1 d))))))) = ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a⊥ →1 d) ∩ (b⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((b⊥ →1 d) →1 d))) ∪ ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((b⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d)))))))
213, 202an 79 . . 3 ((e →1 d) ∩ (e ∪ (f ∩ (((e ∩ f) ∪ ((e →1 d) ∩ (f →1 d))) ∪ (((e ∩ g) ∪ ((e →1 d) ∩ (g →1 d))) ∩ ((f ∩ g) ∪ ((f →1 d) ∩ (g →1 d)))))))) = (((a⊥ →1 d) →1 d) ∩ ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a⊥ →1 d) ∩ (b⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((b⊥ →1 d) →1 d))) ∪ ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((b⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))))))))
222ran 78 . . . . 5 (e ∩ d) = ((a⊥ →1 d) ∩ d)
234ran 78 . . . . 5 (f ∩ d) = ((b⊥ →1 d) ∩ d)
2422, 232or 72 . . . 4 ((e ∩ d) ∪ (f ∩ d)) = (((a⊥ →1 d) ∩ d) ∪ ((b⊥ →1 d) ∩ d))
259ran 78 . . . 4 (g ∩ d) = ((c⊥ →1 d) ∩ d)
2624, 252or 72 . . 3 (((e ∩ d) ∪ (f ∩ d)) ∪ (g ∩ d)) = ((((a⊥ →1 d) ∩ d) ∪ ((b⊥ →1 d) ∩ d)) ∪ ((c⊥ →1 d) ∩ d))
271, 21, 26le3tr2 141 . 2 (((a⊥ →1 d) →1 d) ∩ ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a⊥ →1 d) ∩ (b⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((b⊥ →1 d) →1 d))) ∪ ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((b⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d)))))))) ≤ ((((a⊥ →1 d) ∩ d) ∪ ((b⊥ →1 d) ∩ d)) ∪ ((c⊥ →1 d) ∩ d))
28 u1lem11 780 . . 3 ((a⊥ →1 d) →1 d) = (a →1 d)
29 ax-a2 31 . . . . . . 7 (((a⊥ →1 d) ∩ (b⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((b⊥ →1 d) →1 d))) = ((((a⊥ →1 d) →1 d) ∩ ((b⊥ →1 d) →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d)))
30 u1lem11 780 . . . . . . . . 9 ((b⊥ →1 d) →1 d) = (b →1 d)
3128, 302an 79 . . . . . . . 8 (((a⊥ →1 d) →1 d) ∩ ((b⊥ →1 d) →1 d)) = ((a →1 d) ∩ (b →1 d))
3231ax-r5 38 . . . . . . 7 ((((a⊥ →1 d) →1 d) ∩ ((b⊥ →1 d) →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) = (((a →1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d)))
3329, 32ax-r2 36 . . . . . 6 (((a⊥ →1 d) ∩ (b⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((b⊥ →1 d) →1 d))) = (((a →1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d)))
34 ax-a2 31 . . . . . . . 8 (((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))) = ((((a⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d)))
35 u1lem11 780 . . . . . . . . . 10 ((c⊥ →1 d) →1 d) = (c →1 d)
3628, 352an 79 . . . . . . . . 9 (((a⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d)) = ((a →1 d) ∩ (c →1 d))
3736ax-r5 38 . . . . . . . 8 ((((a⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) = (((a →1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d)))
3834, 37ax-r2 36 . . . . . . 7 (((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))) = (((a →1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d)))
39 ax-a2 31 . . . . . . . 8 (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((b⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))) = ((((b⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d)))
4030, 352an 79 . . . . . . . . 9 (((b⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d)) = ((b →1 d) ∩ (c →1 d))
4140ax-r5 38 . . . . . . . 8 ((((b⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d))) = (((b →1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d)))
4239, 41ax-r2 36 . . . . . . 7 (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((b⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))) = (((b →1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d)))
4338, 422an 79 . . . . . 6 ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((b⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d)))) = ((((a →1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b →1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d))))
4433, 432or 72 . . . . 5 ((((a⊥ →1 d) ∩ (b⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((b⊥ →1 d) →1 d))) ∪ ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((b⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))))) = ((((a →1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) ∪ ((((a →1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b →1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d)))))
4544lan 77 . . . 4 ((b⊥ →1 d) ∩ ((((a⊥ →1 d) ∩ (b⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((b⊥ →1 d) →1 d))) ∪ ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((b⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d)))))) = ((b⊥ →1 d) ∩ ((((a →1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) ∪ ((((a →1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b →1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d))))))
4645lor 70 . . 3 ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a⊥ →1 d) ∩ (b⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((b⊥ →1 d) →1 d))) ∪ ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((b⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))))))) = ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a →1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) ∪ ((((a →1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b →1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d)))))))
4728, 462an 79 . 2 (((a⊥ →1 d) →1 d) ∩ ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a⊥ →1 d) ∩ (b⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((b⊥ →1 d) →1 d))) ∪ ((((a⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((a⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d))) ∩ (((b⊥ →1 d) ∩ (c⊥ →1 d)) ∪ (((b⊥ →1 d) →1 d) ∩ ((c⊥ →1 d) →1 d)))))))) = ((a →1 d) ∩ ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a →1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) ∪ ((((a →1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b →1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d))))))))
48 u1lemab 610 . . . . 5 ((a⊥ →1 d) ∩ d) = ((a⊥ ∩ d) ∪ (a⊥ ⊥ ∩ d))
49 u1lem8 776 . . . . . . 7 ((a →1 d) ∩ (a⊥ →1 d)) = ((a ∩ d) ∪ (a⊥ ∩ d))
50 ax-a2 31 . . . . . . 7 ((a ∩ d) ∪ (a⊥ ∩ d)) = ((a⊥ ∩ d) ∪ (a ∩ d))
51 ax-a1 30 . . . . . . . . 9 a = a⊥ ⊥
5251ran 78 . . . . . . . 8 (a ∩ d) = (a⊥ ⊥ ∩ d)
5352lor 70 . . . . . . 7 ((a⊥ ∩ d) ∪ (a ∩ d)) = ((a⊥ ∩ d) ∪ (a⊥ ⊥ ∩ d))
5449, 50, 533tr 65 . . . . . 6 ((a →1 d) ∩ (a⊥ →1 d)) = ((a⊥ ∩ d) ∪ (a⊥ ⊥ ∩ d))
5554ax-r1 35 . . . . 5 ((a⊥ ∩ d) ∪ (a⊥ ⊥ ∩ d)) = ((a →1 d) ∩ (a⊥ →1 d))
5648, 55ax-r2 36 . . . 4 ((a⊥ →1 d) ∩ d) = ((a →1 d) ∩ (a⊥ →1 d))
57 u1lemab 610 . . . . 5 ((b⊥ →1 d) ∩ d) = ((b⊥ ∩ d) ∪ (b⊥ ⊥ ∩ d))
58 u1lem8 776 . . . . . . 7 ((b →1 d) ∩ (b⊥ →1 d)) = ((b ∩ d) ∪ (b⊥ ∩ d))
59 ax-a2 31 . . . . . . 7 ((b ∩ d) ∪ (b⊥ ∩ d)) = ((b⊥ ∩ d) ∪ (b ∩ d))
60 ax-a1 30 . . . . . . . . 9 b = b⊥ ⊥
6160ran 78 . . . . . . . 8 (b ∩ d) = (b⊥ ⊥ ∩ d)
6261lor 70 . . . . . . 7 ((b⊥ ∩ d) ∪ (b ∩ d)) = ((b⊥ ∩ d) ∪ (b⊥ ⊥ ∩ d))
6358, 59, 623tr 65 . . . . . 6 ((b →1 d) ∩ (b⊥ →1 d)) = ((b⊥ ∩ d) ∪ (b⊥ ⊥ ∩ d))
6463ax-r1 35 . . . . 5 ((b⊥ ∩ d) ∪ (b⊥ ⊥ ∩ d)) = ((b →1 d) ∩ (b⊥ →1 d))
6557, 64ax-r2 36 . . . 4 ((b⊥ →1 d) ∩ d) = ((b →1 d) ∩ (b⊥ →1 d))
6656, 652or 72 . . 3 (((a⊥ →1 d) ∩ d) ∪ ((b⊥ →1 d) ∩ d)) = (((a →1 d) ∩ (a⊥ →1 d)) ∪ ((b →1 d) ∩ (b⊥ →1 d)))
67 u1lemab 610 . . . 4 ((c⊥ →1 d) ∩ d) = ((c⊥ ∩ d) ∪ (c⊥ ⊥ ∩ d))
68 u1lem8 776 . . . . . 6 ((c →1 d) ∩ (c⊥ →1 d)) = ((c ∩ d) ∪ (c⊥ ∩ d))
69 ax-a2 31 . . . . . 6 ((c ∩ d) ∪ (c⊥ ∩ d)) = ((c⊥ ∩ d) ∪ (c ∩ d))
70 ax-a1 30 . . . . . . . 8 c = c⊥ ⊥
7170ran 78 . . . . . . 7 (c ∩ d) = (c⊥ ⊥ ∩ d)
7271lor 70 . . . . . 6 ((c⊥ ∩ d) ∪ (c ∩ d)) = ((c⊥ ∩ d) ∪ (c⊥ ⊥ ∩ d))
7368, 69, 723tr 65 . . . . 5 ((c →1 d) ∩ (c⊥ →1 d)) = ((c⊥ ∩ d) ∪ (c⊥ ⊥ ∩ d))
7473ax-r1 35 . . . 4 ((c⊥ ∩ d) ∪ (c⊥ ⊥ ∩ d)) = ((c →1 d) ∩ (c⊥ →1 d))
7567, 74ax-r2 36 . . 3 ((c⊥ →1 d) ∩ d) = ((c →1 d) ∩ (c⊥ →1 d))
7666, 752or 72 . 2 ((((a⊥ →1 d) ∩ d) ∪ ((b⊥ →1 d) ∩ d)) ∪ ((c⊥ →1 d) ∩ d)) = ((((a →1 d) ∩ (a⊥ →1 d)) ∪ ((b →1 d) ∩ (b⊥ →1 d))) ∪ ((c →1 d) ∩ (c⊥ →1 d)))
7727, 47, 76le3tr2 141 1 ((a →1 d) ∩ ((a⊥ →1 d) ∪ ((b⊥ →1 d) ∩ ((((a →1 d) ∩ (b →1 d)) ∪ ((a⊥ →1 d) ∩ (b⊥ →1 d))) ∪ ((((a →1 d) ∩ (c →1 d)) ∪ ((a⊥ →1 d) ∩ (c⊥ →1 d))) ∩ (((b →1 d) ∩ (c →1 d)) ∪ ((b⊥ →1 d) ∩ (c⊥ →1 d)))))))) ≤ ((((a →1 d) ∩ (a⊥ →1 d)) ∪ ((b →1 d) ∩ (b⊥ →1 d))) ∪ ((c →1 d) ∩ (c⊥ →1 d)))
Colors of variables:    term
This proof depends on syntax axioms:   = wb 1   ≤ wle 2  ⊥ wn 4   ∪ wo 6   ∩ wa 7   →1 wi1 12
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-i1 44  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is used by:  oa4to4u2  974
  Copyright terms: Public domain W3C validator