Theorem coeq12i

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

	Ref	Expression
Hypotheses	coeq12i.1	⊢ 𝐴 = 𝐵
	coeq12i.2	⊢ 𝐶 = 𝐷
Assertion	coeq12i	⊢ ( 𝐴 ∘ 𝐶 ) = ( 𝐵 ∘ 𝐷 )

Proof

Step	Hyp	Ref	Expression
1		coeq12i.1	⊢ 𝐴 = 𝐵
2		coeq12i.2	⊢ 𝐶 = 𝐷
3	1	coeq1i	⊢ ( 𝐴 ∘ 𝐶 ) = ( 𝐵 ∘ 𝐶 )
4	2	coeq2i	⊢ ( 𝐵 ∘ 𝐶 ) = ( 𝐵 ∘ 𝐷 )
5	3 4	eqtri	⊢ ( 𝐴 ∘ 𝐶 ) = ( 𝐵 ∘ 𝐷 )