ax-r3 - Quantum Logic Explorer

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

Axiom ax-r3 439

Description: Orthomodular law - when added to an ortholattice, it makes the ortholattice an orthomodular lattice. See r3a 440 for a more compact version.

**Hypothesis**
Ref	Expression
r3.1

**Assertion**
Ref	Expression
ax-r3

**Detailed syntax breakdown of Axiom ax-r3**
Step	Hyp	Ref	Expression
1		wva	. 2
2		wvb	. 2
3	1, 2	wb 1	1

Colors of variables: term

This axiom is referenced by: r3a 440

W3C validator