Description: An equality transitivity deduction. (Contributed by NM, 21Jun1993)
Ref  Expression  

Hypotheses  syl6eq.1   ( ph > A = B ) 

syl6eq.2   B = C 

Assertion  syl6eq   ( ph > A = C ) 
Step  Hyp  Ref  Expression 

1  syl6eq.1   ( ph > A = B ) 

2  syl6eq.2   B = C 

3  2  a1i   ( ph > B = C ) 
4  1 3  eqtrd   ( ph > A = C ) 