Metamath Proof Explorer


Theorem eqtr3i

Description: An equality transitivity inference. (Contributed by NM, 6-May-1994)

Ref Expression
Hypotheses eqtr3i.1 A=B
eqtr3i.2 A=C
Assertion eqtr3i B=C

Proof

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