Axiom ax-a5 34

Description: Axiom for ortholattices. (Contributed by NM, 9-Aug-1997.)

Assertion

Ref	Expression
ax-a5	(a ∪ (a⊥ ∪ b)⊥ ) = a

Detailed syntax breakdown of Axiom ax-a5

Step	Hyp	Ref	Expression
1		wva	. . 3 term  a
2	1	wn 4	. . . . 5 term  a⊥
3		wvb	. . . . 5 term  b
4	2, 3	wo 6	. . . 4 term  (a⊥ ∪ b)
5	4	wn 4	. . 3 term  (a⊥ ∪ b)⊥
6	1, 5	wo 6	. 2 term  (a ∪ (a⊥ ∪ b)⊥ )
7	6, 1	wb 1	1 wff  (a ∪ (a⊥ ∪ b)⊥ ) = a

This axiom is referenced by:  or0  102  oridm  110  orabs  120  anabs  121  wa5  195