Theorem qlaxr1 5525

Description: One of the conditions showing C_ℋ is an ortholattice. (This corresponds to axiom "ax-r1" in the Quantum Logic Explorer.)

Hypotheses

Ref	Expression
qlaxr1.1	⊢ A ∈ Cℋ
qlaxr1.2	⊢ B ∈ Cℋ
qlaxr1.3	⊢ A = B

Assertion

Ref	Expression
qlaxr1	⊢ B = A

Proof of Theorem qlaxr1

Step	Hyp	Ref	Expression
1		qlaxr1.3	. 2 ⊢ A = B
2	1	cleqcomi 1105	1 ⊢ B = A

Syntax hints:   = wceq 1091   ∈ wcel 1092   C_ℋ cch 4968

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-cleq 1097

metamath.org