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

Theorem r3a 440
Description: Orthomodular law restated. (Contributed by NM, 12-Aug-1997.)
Hypothesis
Ref Expression
r3a.1 1 = (ab)
Assertion
Ref Expression
r3a a = b

Proof of Theorem r3a
StepHypRef Expression
1 r3a.1 . . 3 1 = (ab)
2 df-t 41 . . 3 1 = (aa )
3 df-b 39 . . 3 (ab) = ((ab ) ∪ (ab) )
41, 2, 33tr2 64 . 2 (aa ) = ((ab ) ∪ (ab) )
54ax-r3 439 1 a = b
Colors of variables: term
Syntax hints:   = wb 1   wn 4  tb 5  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