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

Axiom ax-a5 34
Description: Axiom for ortholattices. (Contributed by NM, 9-Aug-1997.)
Assertion
Ref Expression
ax-a5 (a ∪ (ab) ) = 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  (ab)
54wn 4 . . 3 term  (ab)
61, 5wo 6 . 2 term  (a ∪ (ab) )
76, 1wb 1 1 wff  (a ∪ (ab) ) = 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