Metamath Proof Explorer


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 AC=BD

Proof

Step Hyp Ref Expression
1 coeq12i.1 A=B
2 coeq12i.2 C=D
3 1 coeq1i AC=BC
4 2 coeq2i BC=BD
5 3 4 eqtri AC=BD