Axiom ax-a4 32

Description: Axiom for ortholattices.

Assertion

Ref	Expression
ax-a4	(a v (b v b_|_)) = (b v 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 v b_|_)
5	1, 4	wo 6	. 2 term (a v (b v b_|_))
6	5, 4	wb 1	1 wff (a v (b v b_|_)) = (b v b_|_)

This axiom is referenced by:  tt 59  or1 96  wa4 186

metamath.org