Axiom ax-a4 32

Description: Axiom for ortholattices.

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 59  or1 96  wa4 186

metamath.org