QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ax-a4 Unicode version
Axiom ax-a4 33
Description: Axiom for ortholattices.
Assertion
Ref Expression
ax-a4 (a v (b v b')) = (b v b')
Detailed syntax breakdown of Axiom ax-a4
StepHypRef Expression
1 wva . . 3 term a
2 wvb . . . 4 term b
32wn 4 . . . 4 term b'
42, 3wo 6 . . 3 term (b v b')
51, 4wo 6 . 2 term (a v (b v b'))
65, 4wb 1 1 wff (a v (b v b')) = (b v b')
Colors of variables: term
This axiom is referenced by:  tt  60  or1  104  wa4  194  lem4.6.6i1j3  1092  com3iia  1100
  Copyright terms: Public domain W3C validator