Metamath Proof Explorer

Theorem eqtr3di

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998)

Ref Expression
Hypotheses eqtr3di.1 
|- ( ph -> A = B )
eqtr3di.2 
|- A = C
Assertion eqtr3di 
|- ( ph -> B = C )

Proof

Step Hyp Ref Expression
1 eqtr3di.1 
 |-  ( ph -> A = B )
2 eqtr3di.2 
 |-  A = C
3 2 eqcomi 
 |-  C = A
4 3 1 eqtr2id 
 |-  ( ph -> B = C )