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 
$${\u22a2}{A}={B}$$ 


3eqtr4i.2 
$${\u22a2}{C}={A}$$ 


3eqtr4i.3 
$${\u22a2}{D}={B}$$ 

Assertion 
3eqtr4ri 
$${\u22a2}{D}={C}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

3eqtr4i.1 
$${\u22a2}{A}={B}$$ 
2 

3eqtr4i.2 
$${\u22a2}{C}={A}$$ 
3 

3eqtr4i.3 
$${\u22a2}{D}={B}$$ 
4 
3 1

eqtr4i 
$${\u22a2}{D}={A}$$ 
5 
4 2

eqtr4i 
$${\u22a2}{D}={C}$$ 