Theorem coeq1d 5164

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 5160	. 2 |- ( A = B -> ( A o. C ) = ( B o. C ) )
3	1, 2	syl 16	1 |- ( ph -> ( A o. C ) = ( B o. C ) )

Syntax hints:   -> wi 4   = wceq 1379   o. ccom 5003

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-in 3483  df-ss 3490  df-br 4448  df-opab 4506  df-co 5008

This theorem is referenced by:  coeq12d  5167  fcof1oinvd  6184  domss2  7676  mapen  7681  mapfien  7867  mapfienOLD  8138  hashfacen  12469  imasval  14766  cofuass  15116  cofulid  15117  setcinv  15275  catcisolem  15291  catciso  15292  yonedalem3b  15406  gsumvalx  15824  frmdup3  15866  symggrp  16230  f1omvdco2  16279  symggen  16301  psgnunilem1  16324  gsumval3OLD  16711  gsumval3  16714  gsumzf1o  16720  gsumzf1oOLD  16723  psrass1lem  17828  coe1add  18104  evls1fval  18155  evl1sca  18169  evl1var  18171  evls1var  18173  pf1mpf  18187  pf1ind  18190  znval  18367  znle2  18387  tchds  21437  dvnfval  22088  hocsubdir  26408  fcoinver  27161  fcobij  27248  subfacp1lem5  28296  relexpsucr  28556  relexpsucl  28558  relexpcnv  28559  relexpadd  28564  upixp  29851  ltrncoidN  34942  trlcoat  35537  trlcone  35542  cdlemg47a  35548  cdlemg47  35550  ltrnco4  35553  tendovalco  35579  tendoplcbv  35589  tendopl  35590  tendoplass  35597  tendo0pl  35605  tendoipl  35611  cdlemk45  35761  cdlemk53b  35770  cdlemk55a  35773  erngdvlem3  35804  erngdvlem3-rN  35812  tendocnv  35836  dvhvaddcbv  35904  dvhvaddval  35905  dvhvaddass  35912  dicvscacl  36006  cdlemn8  36019  dihordlem7b  36030  dihopelvalcpre  36063