Theorem eqtr4id

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998)

	Ref	Expression
Hypotheses	eqtr4id.2	$$⊢A=B$$
	eqtr4id.1	$$⊢\phi \to C=B$$
Assertion	eqtr4id	$$⊢\phi \to A=C$$

Proof

Step	Hyp	Ref	Expression
1		eqtr4id.2	$$⊢A=B$$
2		eqtr4id.1	$$⊢\phi \to C=B$$
3	1	eqcomi	$$⊢B=A$$
4	2 3	eqtr2di	$$⊢\phi \to A=C$$