ax-wdol - Quantum Logic Explorer

	Quantum Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > QLE Home > Th. List > ax-wdol		GIF version

Axiom ax-wdol 1102

Description: The WDOL (weakly distributive ortholattice) axiom.

**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

Colors of variables: term

This axiom is referenced by: wdcom 1103