Theorem coeq1d 5000

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 4996	. 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 1369   o. ccom 4843

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-in 3334  df-ss 3341  df-br 4292  df-opab 4350  df-co 4848

This theorem is referenced by:  coeq12d  5003  fcof1o  5996  domss2  7469  mapen  7474  mapfien  7656  mapfienOLD  7926  hashfacen  12206  imasval  14448  cofuass  14798  cofulid  14799  setcinv  14957  catcisolem  14973  catciso  14974  yonedalem3b  15088  gsumvalx  15501  frmdup3  15543  symggrp  15904  f1omvdco2  15953  symggen  15975  psgnunilem1  15998  gsumval3OLD  16381  gsumval3  16384  gsumzf1o  16390  gsumzf1oOLD  16393  psrass1lem  17446  coe1add  17717  evls1fval  17753  evl1sca  17767  evl1var  17769  evls1var  17771  pf1mpf  17785  pf1ind  17788  znval  17965  znle2  17985  tchds  20745  dvnfval  21395  hocsubdir  25188  fcobij  26024  subfacp1lem5  27071  relexpsucr  27331  relexpsucl  27333  relexpcnv  27334  relexpadd  27339  upixp  28621  ltrncoidN  33770  trlcoat  34365  trlcone  34370  cdlemg47a  34376  cdlemg47  34378  ltrnco4  34381  tendovalco  34407  tendoplcbv  34417  tendopl  34418  tendoplass  34425  tendo0pl  34433  tendoipl  34439  cdlemk45  34589  cdlemk53b  34598  cdlemk55a  34601  erngdvlem3  34632  erngdvlem3-rN  34640  tendocnv  34664  dvhvaddcbv  34732  dvhvaddval  34733  dvhvaddass  34740  dicvscacl  34834  cdlemn8  34847  dihordlem7b  34858  dihopelvalcpre  34891