Description: An inference from three chained equalities. (Contributed by NM, 29Aug1993)
Ref  Expression  

Hypotheses  3eqtri.1   A = B 

3eqtri.2   B = C 

3eqtri.3   C = D 

Assertion  3eqtri   A = D 
Step  Hyp  Ref  Expression 

1  3eqtri.1   A = B 

2  3eqtri.2   B = C 

3  3eqtri.3   C = D 

4  2 3  eqtri   B = D 
5  1 4  eqtri   A = D 