QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ax-wdol Unicode version
Axiom ax-wdol 1102
Description: The WDOL (weakly distributive ortholattice) axiom.
Assertion
Ref Expression
ax-wdol ((a == b) v (a == b')) = 1
Detailed syntax breakdown of Axiom ax-wdol
StepHypRef Expression
1 wva . . . 4 term a
2 wvb . . . 4 term b
31, 2tb 5 . . 3 term (a == b)
42wn 4 . . . 4 term b'
51, 4tb 5 . . 3 term (a == b')
63, 5wo 6 . 2 term ((a == b) v (a == b'))
7 wt 8 . 2 term 1
86, 7wb 1 1 wff ((a == b) v (a == b')) = 1
Colors of variables: term
This axiom is referenced by:  wdcom  1103
  Copyright terms: Public domain W3C validator