This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem eqtr2i

Description: An equality transitivity inference. (Contributed by NM, 21-Feb-1995)

Ref Expression
Hypotheses eqtr2i.1 ⊢ A = B
eqtr2i.2 ⊢ B = C
Assertion eqtr2i ⊢ C = A

Proof

Step Hyp Ref Expression
1 eqtr2i.1 ⊢ A = B
2 eqtr2i.2 ⊢ B = C
3 1 2 eqtri ⊢ A = C
4 3 eqcomi ⊢ C = A