Axiom ax-a4 33

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

Assertion

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

Detailed syntax breakdown of Axiom ax-a4

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

This axiom is referenced by:  tt  60  or1  104  wa4  194  lem4.6.6i1j3  1094  com3iia  1102