Metamath Proof Explorer
Description: An equality transitivity inference. (Contributed by NM, 26May1993)


Ref 
Expression 

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


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

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

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

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

eqeq2i 
$${\u22a2}{A}={B}\leftrightarrow {A}={C}$$ 
4 
1 3

mpbi 
$${\u22a2}{A}={C}$$ 