Theorem eqtr2i

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

	Ref	Expression
Hypotheses	eqtr2i.1	⊢ 𝐴 = 𝐵
	eqtr2i.2	⊢ 𝐵 = 𝐶
Assertion	eqtr2i	⊢ 𝐶 = 𝐴

Proof

Step	Hyp	Ref	Expression
1		eqtr2i.1	⊢ 𝐴 = 𝐵
2		eqtr2i.2	⊢ 𝐵 = 𝐶
3	1 2	eqtri	⊢ 𝐴 = 𝐶
4	3	eqcomi	⊢ 𝐶 = 𝐴