Theorem coeq12d

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

	Ref	Expression
Hypotheses	coeq12d.1	|- ( ph -> A = B )
	coeq12d.2	|- ( ph -> C = D )
Assertion	coeq12d	|- ( ph -> ( A o. C ) = ( B o. D ) )

Proof

Step	Hyp	Ref	Expression
1		coeq12d.1	|- ( ph -> A = B )
2		coeq12d.2	|- ( ph -> C = D )
3	1	coeq1d	|- ( ph -> ( A o. C ) = ( B o. C ) )
4	2	coeq2d	|- ( ph -> ( B o. C ) = ( B o. D ) )
5	3 4	eqtrd	|- ( ph -> ( A o. C ) = ( B o. D ) )