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

Theorem ka4ot 435
Description: 3-variable version of weakly orthomodular law. It is proved from a weaker-looking equivalent, wom2 434, which in turn is proved from ax-wom 361. (Contributed by NM, 25-Oct-1997.)
Assertion
Ref Expression
ka4ot ((ab) ∪ ((ac) ≡ (bc))) = 1

Proof of Theorem ka4ot
StepHypRef Expression
1 le1 146 . 2 ((ab) ∪ ((ac) ≡ (bc))) ≤ 1
2 wom2 434 . . . . . 6 a ≤ ((ab) ∪ ((ac) ≡ (bc)))
3 wom2 434 . . . . . . 7 b ≤ ((ba) ∪ ((bc) ≡ (ac)))
4 bicom 96 . . . . . . . . 9 (ba) = (ab)
54ax-r4 37 . . . . . . . 8 (ba) = (ab)
6 bicom 96 . . . . . . . 8 ((bc) ≡ (ac)) = ((ac) ≡ (bc))
75, 62or 72 . . . . . . 7 ((ba) ∪ ((bc) ≡ (ac))) = ((ab) ∪ ((ac) ≡ (bc)))
83, 7lbtr 139 . . . . . 6 b ≤ ((ab) ∪ ((ac) ≡ (bc)))
92, 8le2or 168 . . . . 5 (ab) ≤ (((ab) ∪ ((ac) ≡ (bc))) ∪ ((ab) ∪ ((ac) ≡ (bc))))
10 oridm 110 . . . . 5 (((ab) ∪ ((ac) ≡ (bc))) ∪ ((ab) ∪ ((ac) ≡ (bc)))) = ((ab) ∪ ((ac) ≡ (bc)))
119, 10lbtr 139 . . . 4 (ab) ≤ ((ab) ∪ ((ac) ≡ (bc)))
1211leror 152 . . 3 ((ab) ∪ ((ac) ≡ (bc))) ≤ (((ab) ∪ ((ac) ≡ (bc))) ∪ ((ac) ≡ (bc)))
13 ka4lemo 228 . . 3 ((ab) ∪ ((ac) ≡ (bc))) = 1
14 ax-a3 32 . . . 4 (((ab) ∪ ((ac) ≡ (bc))) ∪ ((ac) ≡ (bc))) = ((ab) ∪ (((ac) ≡ (bc)) ∪ ((ac) ≡ (bc))))
15 oridm 110 . . . . 5 (((ac) ≡ (bc)) ∪ ((ac) ≡ (bc))) = ((ac) ≡ (bc))
1615lor 70 . . . 4 ((ab) ∪ (((ac) ≡ (bc)) ∪ ((ac) ≡ (bc)))) = ((ab) ∪ ((ac) ≡ (bc)))
1714, 16ax-r2 36 . . 3 (((ab) ∪ ((ac) ≡ (bc))) ∪ ((ac) ≡ (bc))) = ((ab) ∪ ((ac) ≡ (bc)))
1812, 13, 17le3tr2 141 . 2 1 ≤ ((ab) ∪ ((ac) ≡ (bc)))
191, 18lebi 145 1 ((ab) ∪ ((ac) ≡ (bc))) = 1
Colors of variables: term
Syntax hints:   = wb 1   wn 4  tb 5  wo 6  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:  i3or  497
  Copyright terms: Public domain W3C validator