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 𝐴C
qlaxr2.2 𝐵C
qlaxr2.3 𝐶C
qlaxr2.4 𝐴 = 𝐵
qlaxr2.5 𝐵 = 𝐶
Assertion qlaxr2i 𝐴 = 𝐶

Proof

Step Hyp Ref Expression
1 qlaxr2.1 𝐴C
2 qlaxr2.2 𝐵C
3 qlaxr2.3 𝐶C
4 qlaxr2.4 𝐴 = 𝐵
5 qlaxr2.5 𝐵 = 𝐶
6 4 5 eqtri 𝐴 = 𝐶