Theorem coeq1d 5001

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

Hypothesis

Ref	Expression
coeq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
coeq1d	|- ( ph -> ( A o. C ) = ( B o. C ) )

Proof of Theorem coeq1d

Step	Hyp	Ref	Expression
1		coeq1d.1	. 2 |- ( ph -> A = B )
2		coeq1 4997	. 2 |- ( A = B -> ( A o. C ) = ( B o. C ) )
3	1, 2	syl 17	1 |- ( ph -> ( A o. C ) = ( B o. C ) )

Syntax hints:   -> wi 4   = wceq 1452   o. ccom 4843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-in 3397  df-ss 3404  df-br 4396  df-opab 4455  df-co 4848

This theorem is referenced by:  coeq12d  5004  fcof1oinvd  6209  domss2  7749  mapen  7754  mapfien  7939  hashfacen  12658  relexpsucnnr  13165  relexpsucr  13169  relexpsucnnl  13172  relexpaddnn  13191  imasval  15489  imasvalOLD  15490  cofuass  15872  cofulid  15873  setcinv  16063  catcisolem  16079  catciso  16080  yonedalem3b  16242  gsumvalx  16591  frmdup3lem  16728  symggrp  17119  f1omvdco2  17167  symggen  17189  psgnunilem1  17212  gsumval3  17619  gsumzf1o  17624  psrass1lem  18678  coe1add  18934  evls1fval  18985  evl1sca  18999  evl1var  19001  evls1var  19003  pf1mpf  19017  pf1ind  19020  znval  19183  znle2  19201  tchds  22283  dvnfval  22955  hocsubdir  27519  fcoinver  28290  fcobij  28385  symgfcoeu  28682  subfacp1lem5  29979  mrsubffval  30217  mrsubfval  30218  mrsubrn  30223  elmrsubrn  30230  upixp  32120  ltrncoidN  33764  trlcoat  34361  trlcone  34366  cdlemg47a  34372  cdlemg47  34374  ltrnco4  34377  tendovalco  34403  tendoplcbv  34413  tendopl  34414  tendoplass  34421  tendo0pl  34429  tendoipl  34435  cdlemk45  34585  cdlemk53b  34594  cdlemk55a  34597  erngdvlem3  34628  erngdvlem3-rN  34636  tendocnv  34660  dvhvaddcbv  34728  dvhvaddval  34729  dvhvaddass  34736  dicvscacl  34830  cdlemn8  34843  dihordlem7b  34854  dihopelvalcpre  34887  relexp2  36340  relexpxpnnidm  36366  relexpiidm  36367  relexpmulnn  36372  relexpaddss  36381  trclfvcom  36386  trclfvdecomr  36391  frege131d  36427