QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  r3a Unicode version
Theorem r3a 440
Description: Orthomodular law restated.
Hypothesis
Ref Expression
r3a.1 1 = (a == b)
Assertion
Ref Expression
r3a a = b
Proof of Theorem r3a
StepHypRef Expression
1 r3a.1 . . 3 1 = (a == b)
2 df-t 41 . . 3 1 = (a v a')
3 df-b 39 . . 3 (a == b) = ((a' v b')' v (a v b)')
41, 2, 33tr2 64 . 2 (a v a') = ((a' v b')' v (a v b)')
54ax-r3 439 1 a = b
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   == tb 5   v wo 6  1wt 8
This theorem was proved from axioms:  ax-r1 35  ax-r2 36  ax-r3 439
This theorem depends on definitions:  df-b 39  df-t 41
This theorem is referenced by:  wed  441  lem3.1  443  oi3oa3lem1  732  oi3oa3  733
  Copyright terms: Public domain W3C validator