Theorem coeq12d

Description: Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012)

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

Proof

Step	Hyp	Ref	Expression
1		coeq12d.1	$$⊢\phi \to A=B$$
2		coeq12d.2	$$⊢\phi \to C=D$$
3	1	coeq1d	$$⊢\phi \to A\circ C=B\circ C$$
4	2	coeq2d	$$⊢\phi \to B\circ C=B\circ D$$
5	3 4	eqtrd	$$⊢\phi \to A\circ C=B\circ D$$