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 C
qlaxr2.2 B C
qlaxr2.3 C C
qlaxr2.4 A = B
qlaxr2.5 B = C
Assertion qlaxr2i A = C

Proof

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