**Description:** Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000)

Ref | Expression | ||
---|---|---|---|

Hypothesis | coeq1d.1 | $${\u22a2}{\phi}\to {A}={B}$$ | |

Assertion | coeq2d | $${\u22a2}{\phi}\to {C}\circ {A}={C}\circ {B}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | coeq1d.1 | $${\u22a2}{\phi}\to {A}={B}$$ | |

2 | coeq2 | $${\u22a2}{A}={B}\to {C}\circ {A}={C}\circ {B}$$ | |

3 | 1 2 | syl | $${\u22a2}{\phi}\to {C}\circ {A}={C}\circ {B}$$ |