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

Axiom ax-r3 439
Description: Orthomodular law - when added to an ortholattice, it makes the ortholattice an orthomodular lattice. See r3a 440 for a more compact version. (Contributed by NM, 12-Aug-1997.)
Hypothesis
Ref Expression
r3.1 (cc ) = ((ab ) ∪ (ab) )
Assertion
Ref Expression
ax-r3 a = b

Detailed syntax breakdown of Axiom ax-r3
StepHypRef Expression
1 wva . 2 term  a
2 wvb . 2 term  b
31, 2wb 1 1 wff  a = b
Colors of variables: term
This axiom is referenced by:  r3a  440
  Copyright terms: Public domain W3C validator