Theorem coeq1d 4993

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 4989	. 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 1649   o. ccom 4841

This theorem is referenced by:  coeq12d  4996  fcof1o  5985  domss2  7225  mapen  7230  mapfien  7609  hashfacen  11658  imasval  13692  cofuass  14041  cofulid  14042  setcinv  14200  catcisolem  14216  catciso  14217  yonedalem3b  14331  gsumvalx  14729  frmdup3  14766  symggrp  15058  gsumval3  15469  gsumzf1o  15474  psrass1lem  16397  coe1add  16612  znval  16771  znle2  16789  dvnfval  19761  evl1sca  19903  evl1var  19905  pf1mpf  19925  pf1ind  19928  hocsubdir  23241  subfacp1lem5  24823  relexpsucr  25083  relexpsucl  25085  relexpcnv  25086  relexpadd  25091  upixp  26321  f1omvdco2  27259  symggen  27279  psgnunilem1  27284  ltrncoidN  30610  trlcoat  31205  trlcone  31210  cdlemg47a  31216  cdlemg47  31218  ltrnco4  31221  tendovalco  31247  tendoplcbv  31257  tendopl  31258  tendoplass  31265  tendo0pl  31273  tendoipl  31279  cdlemk45  31429  cdlemk53b  31438  cdlemk55a  31441  erngdvlem3  31472  erngdvlem3-rN  31480  tendocnv  31504  dvhvaddcbv  31572  dvhvaddval  31573  dvhvaddass  31580  dicvscacl  31674  cdlemn8  31687  dihordlem7b  31698  dihopelvalcpre  31731

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-in 3287  df-ss 3294  df-br 4173  df-opab 4227  df-co 4846