QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ax-r3 Structured version   Unicode 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.
Hypothesis
Ref Expression
r3.1 (c v c') = ((a' v b')' v (a v b)')
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