Theorem eqtr2i

Description: An equality transitivity inference. (Contributed by NM, 21-Feb-1995)

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

Proof

Step	Hyp	Ref	Expression
1		eqtr2i.1	|- A = B
2		eqtr2i.2	|- B = C
3	1 2	eqtri	|- A = C
4	3	eqcomi	|- C = A