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

Metamath Proof Explorer

Theorem eqtr4i

Description: An equality transitivity inference. (Contributed by NM, 26-May-1993)

Ref Expression
Hypotheses eqtr4i.1 
|- A = B
eqtr4i.2 
|- C = B
Assertion eqtr4i 
|- A = C

Proof

Step Hyp Ref Expression
1 eqtr4i.1 
 |-  A = B
2 eqtr4i.2 
 |-  C = B
3 2 eqcomi 
 |-  B = C
4 1 3 eqtri 
 |-  A = C