Theorem coeq12i

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

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

Proof

Step	Hyp	Ref	Expression
1		coeq12i.1	|- A = B
2		coeq12i.2	|- C = D
3	1	coeq1i	|- ( A o. C ) = ( B o. C )
4	2	coeq2i	|- ( B o. C ) = ( B o. D )
5	3 4	eqtri	|- ( A o. C ) = ( B o. D )