QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ax-a5 Unicode version
Axiom ax-a5 34
Description: Axiom for ortholattices.
Assertion
Ref Expression
ax-a5 (a v (a' v b)') = a
Detailed syntax breakdown of Axiom ax-a5
StepHypRef Expression
1 wva . . 3 term a
21wn 4 . . . . 5 term a'
3 wvb . . . . 5 term b
42, 3wo 6 . . . 4 term (a' v b)
54wn 4 . . 3 term (a' v b)'
61, 5wo 6 . 2 term (a v (a' v b)')
76, 1wb 1 1 wff (a v (a' v b)') = a
Colors of variables: term
This axiom is referenced by:  or0  102  oridm  110  orabs  120  anabs  121  wa5  195
  Copyright terms: Public domain W3C validator