Theorem oveqd 7386

Description: Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.)

Hypothesis

Ref	Expression
oveq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
oveqd	⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))

Proof of Theorem oveqd

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		oveq 7375	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))

Syntax hints:   → wi 4   = wceq 1540  (class class class)co 7369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372

This theorem is referenced by:  oveq123d  7390  oveqdr  7397  csbov  7414  csbov12g  7415  ovmpodxf  7519  oprssov  7538  2mpo0  7618  ofeqd  7635  mptmpoopabbrd  8038  mptmpoopabbrdOLD  8039  mptmpoopabovd  8040  el2mpocsbcl  8041  fnmpoovd  8043  frecseq123  8238  ruclem1  16176  vdwapval  16921  vdwapid1  16923  vdwmc2  16927  vdwpc  16928  vdwlem5  16933  vdwlem8  16936  vdwlem13  16941  prdsval  17395  prdsdsval2  17424  pwsplusgval  17430  pwsmulrval  17431  pwsvscafval  17434  imasval  17451  iscat  17614  iscatd  17615  catidex  17616  catideu  17617  cidfval  17618  cidval  17619  catidd  17622  iscatd2  17623  catlid  17625  catrid  17626  homffval  17632  homfeqd  17637  homfeqval  17639  comfffval  17640  comffval  17641  comfeq  17648  comfeqd  17649  comfeqval  17650  catpropd  17651  oppcval  17655  oppcco  17659  monfval  17675  ismon  17676  oppcmon  17681  oppcepi  17682  sectffval  17693  sectfval  17694  invffval  17701  isoval  17708  dfiso2  17715  isofn  17718  invisoinvl  17733  invcoisoid  17735  isocoinvid  17736  issubc  17778  issubc3  17792  isfunc  17807  cofuval  17825  cofuval2  17830  funcres  17839  funcres2b  17840  funcres2  17841  idfusubc  17843  funcres2c  17846  isfull  17855  isfth  17859  fullres2c  17884  natfval  17892  isnat  17893  fucval  17904  fucco  17908  fucpropd  17923  initoval  17936  termoval  17937  homarcl  17971  coafval  18007  resssetc  18035  resscatc  18052  catciso  18054  xpcval  18119  1stfval  18133  2ndfval  18136  prfval  18141  prfcl  18145  evlfval  18159  curfval  18165  curf1cl  18170  curfcl  18174  uncf1  18178  uncf2  18179  diag12  18186  diag2  18187  curf2ndf  18189  hofval  18194  hof1  18196  hof2fval  18197  hofcl  18201  yon12  18207  yon2  18208  hofpropd  18209  joinval  18317  meetval  18331  isdlat  18464  plusffval  18556  ismgmd  18562  issstrmgm  18563  grpidval  18571  grpidd  18581  gsumvalx  18586  gsumpropd  18588  gsumress  18592  ismgmhm  18606  issubmgm  18612  resmgmhm  18621  resmgmhm2  18622  resmgmhm2b  18623  issgrpd  18640  ismndd  18666  issubmnd  18671  submnd0  18673  ismhm  18695  issubm  18713  resmhm  18730  resmhm2  18731  resmhm2b  18732  mhmimalem  18734  isgrp  18854  isgrpd2e  18870  grpidd2  18892  grpinvfval  18893  grpinvfvalALT  18894  imasgrp2  18970  imasgrp  18971  subg0  19047  subginv  19048  subgcl  19051  issubgrpd2  19057  isnsg  19070  isghm  19130  isghmOLD  19131  resghm  19147  isga  19206  subgga  19215  gasubg  19217  cntzfval  19235  resscntz  19248  odfval  19447  odfvalALT  19448  gexval  19493  lsmfval  19553  lsmvalx  19554  oppglsm  19557  subglsm  19588  pj1fval  19609  efgtval  19638  iscmn  19704  iscmnd  19709  submcmn2  19754  imasabl  19791  iscyg  19794  cycsubmcmn  19804  isomnd  20038  submomnd  20047  prdsmgp  20072  rngpropd  20095  ringurd  20106  issrg  20109  isring  20158  ringidss  20198  mulgass3  20274  dvdsrval  20282  rdivmuldivd  20334  isirred  20340  rnghmval  20361  islring  20461  lringuplu  20465  subrngmcl  20478  subrg1  20503  subrgdvds  20507  subrguss  20508  subrginv  20509  subrgdv  20510  subrgunit  20511  subrgugrp  20512  rnghmresel  20541  rngchom  20544  rngcco  20548  rnghmsubcsetclem1  20552  rhmresel  20570  ringchom  20573  ringcco  20577  rhmsubcsetclem1  20581  rhmsubcrngclem1  20587  rrgval  20618  isdrngd  20686  isdrngrd  20687  isdrngdOLD  20688  isdrngrdOLD  20689  abvfval  20731  isabvd  20733  issrngd  20776  isorng  20782  suborng  20797  islmod  20803  islmodd  20805  scaffval  20819  lmodpropd  20864  lssset  20872  islssd  20874  prdslmodd  20908  islmhm  20967  reslmhm  20992  reslmhm2  20993  reslmhm2b  20994  islbs  21016  rlmvneg  21146  rnglidlmmgm  21188  rnglidlmsgrp  21189  rnglidlrng  21190  rngqiprngghmlem3  21232  rngqiprngimfolem  21233  rngqiprnglinlem1  21234  rngqiprngimf1  21243  rngqiprnglin  21245  rng2idl1cntr  21248  rngqiprngfulem5  21258  irinitoringc  21422  isphl  21571  ipffval  21591  isphld  21597  phssipval  21600  phssip  21601  phlssphl  21602  ocvfval  21609  isobs  21663  frlmplusgval  21707  frlmsubgval  21708  frlmvscafval  21709  frlmip  21721  frlmipval  21722  frlmup1  21741  lsslindf  21773  isassa  21799  isassad  21808  sraassab  21811  assamulgscmlem2  21843  psrval  21858  resspsradd  21918  resspsrmul  21919  resspsrvsca  21920  mplmon2mul  22010  ply1coe  22219  ply1chr  22227  lply1binomsc  22232  evl1expd  22266  evl1scvarpw  22284  asclply1subcl  22295  mamufval  22313  matplusg2  22348  matvsca2  22349  matplusgcell  22354  matsubgcell  22355  matinvgcell  22356  matvscacell  22357  matmulcell  22366  mpomatmul  22367  mat1  22368  mattposm  22380  mat1dimmul  22397  dmatmul  22418  dmatcrng  22423  scmataddcl  22437  scmatsubcl  22438  scmatcrng  22442  smatvscl  22445  scmatghm  22454  scmatmhm  22455  mvmulfval  22463  ma1repveval  22492  mdetrlin  22523  mdetrsca  22524  mdetmul  22544  madurid  22565  minmar1cl  22572  smadiadetglem1  22592  smadiadetr  22596  matinv  22598  slesolinv  22601  slesolinvbi  22602  cramerimplem3  22606  cpmatacl  22637  mat2pmatghm  22651  decpmatmullem  22692  decpmatmul  22693  pmatcollpw1lem1  22695  pmatcollpw2lem  22698  pmatcollpwlem  22701  pmatcollpw3lem  22704  mply1topmatval  22725  mp2pm2mplem1  22727  mp2pm2mplem4  22730  mp2pm2mplem5  22731  mp2pm2mp  22732  chpmat1d  22757  chpscmatgsummon  22766  chfacfpmmulgsum2  22786  xkocnv  23735  submtmd  24025  prdsdsf  24289  ressprdsds  24293  blfvalps  24305  prdsxmslem2  24451  tmsxpsval  24460  ngpds  24526  sgrimval  24554  subgngp  24557  tngngp  24576  tngngp3  24578  isnlm  24597  lssnlm  24623  isphtpy  24914  isphtpc  24927  pi1cpbl  24978  pi1addf  24981  pi1addval  24982  pi1grplem  24983  clmsub  25014  clmvsass  25023  clmvsdir  25025  isclmp  25031  cvsdiv  25066  iscph  25104  cphdir  25139  cphdi  25140  cph2di  25141  cph2subdi  25144  cphass  25145  tcphval  25152  ipcau2  25168  tcphcphlem1  25169  tcphcphlem2  25170  cphsscph  25185  caufval  25209  rrxip  25324  rrxvsca  25328  rrxplusgvscavalb  25329  rrxdsfival  25347  ehleudisval  25353  dvlip2  25934  q1pval  26094  r1pval  26097  dvntaylp  26313  efabl  26493  efsubm  26494  dchrmul  27193  seqseq123d  28221  istrkgc  28435  istrkgb  28436  istrkgcb  28437  istrkge  28438  istrkgl  28439  istrkgld  28440  iscgrg  28493  isismt  28515  tglngval  28532  legval  28565  ishlg  28583  mirval  28636  israg  28678  ishpg  28740  lmif  28766  islmib  28768  isinag  28819  ttgval  28856  wksonproplem  29684  wspthsnon  29833  iswwlksnon  29834  iswspthsnon  29837  isconngr  30169  isconngr1  30170  grpodivval  30515  dipfval  30682  ipval  30683  sspgval  30709  sspsval  30711  lnoval  30732  ajfval  30789  dipdir  30822  dipass  30825  htth  30898  ressmulgnn0d  33029  inftmrel  33150  isinftm  33151  isslmd  33172  elrgspnlem1  33210  erlval  33226  rlocval  33227  rlocaddval  33236  rlocmulval  33237  subrdom  33252  resv1r  33305  lsmidllsp  33365  idlinsubrg  33396  prmidlval  33402  idlsrgval  33468  idlsrg0g  33471  rprmval  33481  ressply1evls1  33528  drgextlsp  33583  fedgmullem1  33619  fedgmullem2  33620  fedgmul  33621  extdg1id  33655  fldextrspunlsplem  33662  fldextrspunlsp  33663  algextdeglem8  33708  smatlem  33781  submatminr1  33794  metidval  33874  pstmval  33879  pstmfval  33880  zlm0  33944  zlm1  33945  sitmval  34334  breprexp  34618  istrkg2d  34651  afsval  34656  mclsrcl  35542  mppsval  35553  bj-endval  37297  matunitlindflem2  37605  istotbnd  37757  isbnd  37768  rrnequiv  37823  isrngo  37885  rngohomval  37952  idlval  38001  pridlval  38021  lflset  39046  islfld  39049  ldualvadd  39116  ldualsmul  39122  ldualvs  39124  isopos  39167  cmtfvalN  39197  iscvlat  39310  ishlat1  39339  lineset  39726  psubspset  39732  paddfval  39785  paddval  39786  ltrnfset  40105  trnfsetN  40143  trlfset  40148  tgrpov  40736  erngplus  40791  erngmul  40794  erngplus-rN  40799  erngmul-rN  40802  erngdvlem3  40978  erngdvlem4  40979  erng0g  40982  erngdvlem3-rN  40986  erngdvlem4-rN  40987  dvaplusg  40997  dvamulr  41000  dvavadd  41003  dvavsca  41005  dvalveclem  41013  dvhmulr  41074  dvhfvadd  41079  dvhvadd  41080  dvhopvadd2  41082  dvhvaddcl  41083  dvhvaddcomN  41084  dvhvsca  41089  dvhlveclem  41096  dvh0g  41099  djavalN  41123  diblsmopel  41159  dicvaddcl  41178  cdlemn6  41190  dihffval  41218  dihopelvalcpre  41236  djhval  41386  lcdvaddval  41586  lcdsmul  41590  lcdvsval  41592  lcdlkreq2N  41611  hvmapffval  41746  hvmapfval  41747  hdmap1fval  41784  hgmapffval  41873  hgmapfval  41874  hgmapadd  41882  hlhilipval  41937  hlhilhillem  41948  isprimroot  42075  aks6d1c1p4  42093  idomnnzpownz  42114  aks6d1c5lem1  42118  aks6d1c5lem3  42119  aks6d1c5lem2  42120  aks5lem3a  42171  unitscyglem5  42181  rhmpsr1  42535  selvvvval  42567  mhphf2  42580  prjspval  42585  prjspner1  42608  sn-isghm  42655  mnringvald  44196  ioorrnopnlem  46296  hoidmvval0b  46582  hoidmvlelem2  46588  hoidmvlelem3  46589  hoidmvle  46592  ovnhoi  46595  hoiqssbl  46617  hspmbllem2  46619  vonioo  46674  vonicc  46677  zlidlring  48216  uzlidlring  48217  ovmpordxf  48321  lincop  48391  lincval  48392  lincsum  48412  lincscm  48413  lmod1lem2  48471  lmod1lem3  48472  lmod1lem4  48473  ldepsnlinc  48491  lines  48714  line  48715  rrxlines  48716  rrxline  48717  spheres  48729  fvconstr  48844  fvconstrn0  48845  fvconstr2  48846  catprs  48994  sectrcl2  49006  invrcl2  49008  invfn  49013  isorcl2  49017  sectpropdlem  49019  invpropdlem  49021  isopropdlem  49023  cicpropdlem  49032  iinfconstbas  49049  nelsubclem  49050  nelsubc3lem  49053  ssccatid  49055  resccatlem  49056  cofu2a  49078  cofid2a  49096  cofid2  49098  cofidf2a  49100  cofidf2  49103  oppf2  49123  upfval  49159  upfval2  49160  upfval3  49161  upeu3  49178  upeu4  49179  oppcup3  49192  natoppfb  49214  swapfval  49245  swapf2a  49254  1stfpropd  49273  2ndfpropd  49274  cofuswapf2  49278  tposcurf12  49281  tposcurf2  49283  tposcurf2cl  49285  fucofvalg  49301  fuco11b  49320  fuco23a  49335  precofval3  49354  prcofpropd  49362  catcrcl2  49379  opf12  49387  fucoppcco  49392  thincmod  49413  isthincd2lem2  49418  isthincd  49419  dfinito4  49484  mndtcco2  49569  mndtccatid  49570  oppgoppchom  49573  oppgoppcco  49574  grptcmon  49576  grptcepi  49577  2arwcatlem2  49579  2arwcatlem3  49580  2arwcatlem4  49581  2arwcat  49583  lanrcl  49604  ranrcl  49605  rellan  49606  relran  49607  concom  49646  coccom  49647