Metamath Proof Explorer
Description: An inference from three chained equalities. (Contributed by NM, 29Aug1993)


Ref 
Expression 

Hypotheses 
3eqtri.1 
$${\u22a2}{A}={B}$$ 


3eqtri.2 
$${\u22a2}{B}={C}$$ 


3eqtri.3 
$${\u22a2}{C}={D}$$ 

Assertion 
3eqtri 
$${\u22a2}{A}={D}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

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

3eqtri.2 
$${\u22a2}{B}={C}$$ 
3 

3eqtri.3 
$${\u22a2}{C}={D}$$ 
4 
2 3

eqtri 
$${\u22a2}{B}={D}$$ 
5 
1 4

eqtri 
$${\u22a2}{A}={D}$$ 