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

Theorem oml 445
Description: Orthomodular law. Compare Th. 1 of Pavicic 1987.
Assertion
Ref Expression
oml (a v (a' ^ (a v b))) = (a v b)

Proof of Theorem oml
StepHypRef Expression
1 omlem1 127 . 2 ((a v (a' ^ (a v b))) v (a v b)) = (a v b)
2 omlem2 128 . 2 ((a v b)' v (a v (a' ^ (a v b)))) = 1
31, 2lem3.1 443 1 (a v (a' ^ (a v b))) = (a v b)
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7
This theorem is referenced by:  omln  446  oml5  449  oml2  451  ud1lem2  561  ud2lem2  564  ud3lem2  571  ud4lem2  582  ud5lem3  594  test  802  2oalem1  825  oas  925  oat  927  lem4.6.6i2j4  1095
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42
  Copyright terms: Public domain W3C validator