Metamath Proof Explorer
Description: An inference from three chained equalities. (Contributed by NM, 2Sep1995) (Proof shortened by Andrew Salmon, 25May2011)


Ref 
Expression 

Hypotheses 
3eqtr4i.1 
 A = B 


3eqtr4i.2 
 C = A 


3eqtr4i.3 
 D = B 

Assertion 
3eqtr4ri 
 D = C 
Proof
Step 
Hyp 
Ref 
Expression 
1 

3eqtr4i.1 
 A = B 
2 

3eqtr4i.2 
 C = A 
3 

3eqtr4i.3 
 D = B 
4 
3 1

eqtr4i 
 D = A 
5 
4 2

eqtr4i 
 D = C 