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

Axiom ax-a4 33
Description: Axiom for ortholattices. (Contributed by NM, 9-Aug-1997.)
Assertion
Ref Expression
ax-a4 (a ∪ (bb )) = (bb )

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  (bb )
51, 4wo 6 . 2 term  (a ∪ (bb ))
65, 4wb 1 1 wff  (a ∪ (bb )) = (bb )
Colors of variables: term
This axiom is referenced by:  tt  60  or1  104  wa4  194  lem4.6.6i1j3  1094  com3iia  1102
  Copyright terms: Public domain W3C validator