Theorem r3a 440

Description: Orthomodular law restated. (Contributed by NM, 12-Aug-1997.)

Hypothesis

Ref	Expression
r3a.1	1 = (a ≡ b)

Assertion

Ref	Expression
r3a	a = b

Proof of Theorem r3a

Step	Hyp	Ref	Expression
1		r3a.1	. . 3 1 = (a ≡ b)
2		df-t 41	. . 3 1 = (a ∪ a⊥ )
3		df-b 39	. . 3 (a ≡ b) = ((a⊥ ∪ b⊥ )⊥ ∪ (a ∪ b)⊥ )
4	1, 2, 3	3tr2 64	. 2 (a ∪ a⊥ ) = ((a⊥ ∪ b⊥ )⊥ ∪ (a ∪ b)⊥ )
5	4	ax-r3 439	1 a = b

Syntax hints:   = wb 1  ^⊥ wn 4   ≡ tb 5   ∪ wo 6  1wt 8

This theorem was proved from axioms:  ax-r1 35  ax-r2 36  ax-r3 439

This theorem depends on definitions:  df-b 39  df-t 41

This theorem is referenced by:  wed  441  lem3.1  443  oi3oa3lem1  732  oi3oa3  733