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	(c v c') = ((a' v b')' v (a v 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

Copyright terms: Public domain