Theorem eqtri

Description: An equality transitivity inference. (Contributed by NM, 26-May-1993)

	Ref	Expression
Hypotheses	eqtri.1	|- A = B
	eqtri.2	|- B = C
Assertion	eqtri	|- A = C

Proof

Step	Hyp	Ref	Expression
1		eqtri.1	|- A = B
2		eqtri.2	|- B = C
3	2	eqeq2i	|- ( A = B <-> A = C )
4	1 3	mpbi	|- A = C