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. (Contributed by NM, 12-Aug-1997.)

Hypothesis

Ref	Expression
r3.1	(c ∪ c⊥ ) = ((a⊥ ∪ b⊥ )⊥ ∪ (a ∪ b)⊥ )

Assertion

Ref	Expression
ax-r3	a = b

Detailed syntax breakdown of Axiom ax-r3

Step	Hyp	Ref	Expression
1		wva	. 2 term  a
2		wvb	. 2 term  b
3	1, 2	wb 1	1 wff  a = b

This axiom is referenced by:  r3a  440