Metamath Proof Explorer


Theorem qlaxr2i

Description: One of the conditions showing CH is an ortholattice. (This corresponds to axiom "ax-r2" in the Quantum Logic Explorer.) (Contributed by NM, 4-Aug-2004) (New usage is discouraged.)

Ref Expression
Hypotheses qlaxr2.1
|- A e. CH
qlaxr2.2
|- B e. CH
qlaxr2.3
|- C e. CH
qlaxr2.4
|- A = B
qlaxr2.5
|- B = C
Assertion qlaxr2i
|- A = C

Proof

Step Hyp Ref Expression
1 qlaxr2.1
 |-  A e. CH
2 qlaxr2.2
 |-  B e. CH
3 qlaxr2.3
 |-  C e. CH
4 qlaxr2.4
 |-  A = B
5 qlaxr2.5
 |-  B = C
6 4 5 eqtri
 |-  A = C