Quantum Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  QLE Home  >  Th. List  >  axoa4a GIF version

Theorem axoa4a 1037
 Description: Proper 4-variable OA law variant.
Assertion
Ref Expression
axoa4a ((a1 d) ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ (((ad) ∪ (bd)) ∪ (cd))

Proof of Theorem axoa4a
StepHypRef Expression
1 id 59 . 2 (a1 d) = (a1 d)
2 id 59 . 2 (b1 d) = (b1 d)
3 id 59 . 2 (c1 d) = (c1 d)
4 leo 158 . . . 4 a ≤ (a ∪ (ad))
5 df-i1 44 . . . . . 6 (a1 d) = (a ∪ (ad))
65ax-r1 35 . . . . 5 (a ∪ (ad)) = (a1 d)
7 ax-a1 30 . . . . 5 (a1 d) = (a1 d)
86, 7ax-r2 36 . . . 4 (a ∪ (ad)) = (a1 d)
94, 8lbtr 139 . . 3 a ≤ (a1 d)
10 leo 158 . . . 4 b ≤ (b ∪ (bd))
11 df-i1 44 . . . . . 6 (b1 d) = (b ∪ (bd))
1211ax-r1 35 . . . . 5 (b ∪ (bd)) = (b1 d)
13 ax-a1 30 . . . . 5 (b1 d) = (b1 d)
1412, 13ax-r2 36 . . . 4 (b ∪ (bd)) = (b1 d)
1510, 14lbtr 139 . . 3 b ≤ (b1 d)
16 leo 158 . . . 4 c ≤ (c ∪ (cd))
17 df-i1 44 . . . . . 6 (c1 d) = (c ∪ (cd))
1817ax-r1 35 . . . . 5 (c ∪ (cd)) = (c1 d)
19 ax-a1 30 . . . . 5 (c1 d) = (c1 d)
2018, 19ax-r2 36 . . . 4 (c ∪ (cd)) = (c1 d)
2116, 20lbtr 139 . . 3 c ≤ (c1 d)
229, 15, 21oa6 1036 . 2 (((a ∪ (a1 d) ) ∩ (b ∪ (b1 d) )) ∩ (c ∪ (c1 d) )) ≤ ((a1 d) ∪ (a ∩ (b ∪ (((ab ) ∩ ((a1 d) ∪ (b1 d) )) ∩ (((ac ) ∩ ((a1 d) ∪ (c1 d) )) ∪ ((bc ) ∩ ((b1 d) ∪ (c1 d) )))))))
231, 2, 3, 22oa6to4 958 1 ((a1 d) ∩ (a ∪ (b ∩ (((ab) ∪ ((a1 d) ∩ (b1 d))) ∪ (((ac) ∪ ((a1 d) ∩ (c1 d))) ∩ ((bc) ∪ ((b1 d) ∩ (c1 d)))))))) ≤ (((ad) ∪ (bd)) ∪ (cd))
 Colors of variables: term Syntax hints:   ≤ wle 2  ⊥ wn 4   ∪ wo 6   ∩ wa 7   →1 wi1 12 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-r3 439  ax-4oa 1033 This theorem 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 referenced by:  4oa  1039
 Copyright terms: Public domain W3C validator