Axiom ax-wdol 1104

Description: The WDOL (weakly distributive ortholattice) axiom. (Contributed by NM, 4-Mar-2006.)

Assertion

Ref	Expression
ax-wdol	((a ≡ b) ∪ (a ≡ b⊥ )) = 1

Detailed syntax breakdown of Axiom ax-wdol

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

This axiom is referenced by:  wdcom  1105