Theorem oveqd 7363

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 7352	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))

Syntax hints:   → wi 4   = wceq 1541  (class class class)co 7346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  oveq123d  7367  oveqdr  7374  csbov  7391  csbov12g  7392  ovmpodxf  7496  oprssov  7515  2mpo0  7595  ofeqd  7612  mptmpoopabbrd  8012  mptmpoopabbrdOLD  8013  mptmpoopabovd  8014  el2mpocsbcl  8015  fnmpoovd  8017  frecseq123  8212  ruclem1  16140  vdwapval  16885  vdwapid1  16887  vdwmc2  16891  vdwpc  16892  vdwlem5  16897  vdwlem8  16900  vdwlem13  16905  prdsval  17359  prdsdsval2  17388  pwsplusgval  17394  pwsmulrval  17395  pwsvscafval  17398  imasval  17415  iscat  17578  iscatd  17579  catidex  17580  catideu  17581  cidfval  17582  cidval  17583  catidd  17586  iscatd2  17587  catlid  17589  catrid  17590  homffval  17596  homfeqd  17601  homfeqval  17603  comfffval  17604  comffval  17605  comfeq  17612  comfeqd  17613  comfeqval  17614  catpropd  17615  oppcval  17619  oppcco  17623  monfval  17639  ismon  17640  oppcmon  17645  oppcepi  17646  sectffval  17657  sectfval  17658  invffval  17665  isoval  17672  dfiso2  17679  isofn  17682  invisoinvl  17697  invcoisoid  17699  isocoinvid  17700  issubc  17742  issubc3  17756  isfunc  17771  cofuval  17789  cofuval2  17794  funcres  17803  funcres2b  17804  funcres2  17805  idfusubc  17807  funcres2c  17810  isfull  17819  isfth  17823  fullres2c  17848  natfval  17856  isnat  17857  fucval  17868  fucco  17872  fucpropd  17887  initoval  17900  termoval  17901  homarcl  17935  coafval  17971  resssetc  17999  resscatc  18016  catciso  18018  xpcval  18083  1stfval  18097  2ndfval  18100  prfval  18105  prfcl  18109  evlfval  18123  curfval  18129  curf1cl  18134  curfcl  18138  uncf1  18142  uncf2  18143  diag12  18150  diag2  18151  curf2ndf  18153  hofval  18158  hof1  18160  hof2fval  18161  hofcl  18165  yon12  18171  yon2  18172  hofpropd  18173  joinval  18281  meetval  18295  isdlat  18428  plusffval  18554  ismgmd  18560  issstrmgm  18561  grpidval  18569  grpidd  18579  gsumvalx  18584  gsumpropd  18586  gsumress  18590  ismgmhm  18604  issubmgm  18610  resmgmhm  18619  resmgmhm2  18620  resmgmhm2b  18621  issgrpd  18638  ismndd  18664  issubmnd  18669  submnd0  18671  ismhm  18693  issubm  18711  resmhm  18728  resmhm2  18729  resmhm2b  18730  mhmimalem  18732  isgrp  18852  isgrpd2e  18868  grpidd2  18890  grpinvfval  18891  grpinvfvalALT  18892  imasgrp2  18968  imasgrp  18969  subg0  19045  subginv  19046  subgcl  19049  issubgrpd2  19055  isnsg  19067  isghm  19127  isghmOLD  19128  resghm  19144  isga  19203  subgga  19212  gasubg  19214  cntzfval  19232  resscntz  19245  odfval  19444  odfvalALT  19445  gexval  19490  lsmfval  19550  lsmvalx  19551  oppglsm  19554  subglsm  19585  pj1fval  19606  efgtval  19635  iscmn  19701  iscmnd  19706  submcmn2  19751  imasabl  19788  iscyg  19791  cycsubmcmn  19801  isomnd  20035  submomnd  20044  prdsmgp  20069  rngpropd  20092  ringurd  20103  issrg  20106  isring  20155  ringidss  20195  mulgass3  20271  dvdsrval  20279  rdivmuldivd  20331  isirred  20337  rnghmval  20358  islring  20455  lringuplu  20459  subrngmcl  20472  subrg1  20497  subrgdvds  20501  subrguss  20502  subrginv  20503  subrgdv  20504  subrgunit  20505  subrgugrp  20506  rnghmresel  20535  rngchom  20538  rngcco  20542  rnghmsubcsetclem1  20546  rhmresel  20564  ringchom  20567  ringcco  20571  rhmsubcsetclem1  20575  rhmsubcrngclem1  20581  rrgval  20612  isdrngd  20680  isdrngrd  20681  isdrngdOLD  20682  isdrngrdOLD  20683  abvfval  20725  isabvd  20727  issrngd  20770  isorng  20776  suborng  20791  islmod  20797  islmodd  20799  scaffval  20813  lmodpropd  20858  lssset  20866  islssd  20868  prdslmodd  20902  islmhm  20961  reslmhm  20986  reslmhm2  20987  reslmhm2b  20988  islbs  21010  rlmvneg  21140  rnglidlmmgm  21182  rnglidlmsgrp  21183  rnglidlrng  21184  rngqiprngghmlem3  21226  rngqiprngimfolem  21227  rngqiprnglinlem1  21228  rngqiprngimf1  21237  rngqiprnglin  21239  rng2idl1cntr  21242  rngqiprngfulem5  21252  irinitoringc  21416  isphl  21565  ipffval  21585  isphld  21591  phssipval  21594  phssip  21595  phlssphl  21596  ocvfval  21603  isobs  21657  frlmplusgval  21701  frlmsubgval  21702  frlmvscafval  21703  frlmip  21715  frlmipval  21716  frlmup1  21735  lsslindf  21767  isassa  21793  isassad  21802  sraassab  21805  assamulgscmlem2  21837  psrval  21852  resspsradd  21912  resspsrmul  21913  resspsrvsca  21914  mplmon2mul  22004  ply1coe  22213  ply1chr  22221  lply1binomsc  22226  evl1expd  22260  evl1scvarpw  22278  asclply1subcl  22289  mamufval  22307  matplusg2  22342  matvsca2  22343  matplusgcell  22348  matsubgcell  22349  matinvgcell  22350  matvscacell  22351  matmulcell  22360  mpomatmul  22361  mat1  22362  mattposm  22374  mat1dimmul  22391  dmatmul  22412  dmatcrng  22417  scmataddcl  22431  scmatsubcl  22432  scmatcrng  22436  smatvscl  22439  scmatghm  22448  scmatmhm  22449  mvmulfval  22457  ma1repveval  22486  mdetrlin  22517  mdetrsca  22518  mdetmul  22538  madurid  22559  minmar1cl  22566  smadiadetglem1  22586  smadiadetr  22590  matinv  22592  slesolinv  22595  slesolinvbi  22596  cramerimplem3  22600  cpmatacl  22631  mat2pmatghm  22645  decpmatmullem  22686  decpmatmul  22687  pmatcollpw1lem1  22689  pmatcollpw2lem  22692  pmatcollpwlem  22695  pmatcollpw3lem  22698  mply1topmatval  22719  mp2pm2mplem1  22721  mp2pm2mplem4  22724  mp2pm2mplem5  22725  mp2pm2mp  22726  chpmat1d  22751  chpscmatgsummon  22760  chfacfpmmulgsum2  22780  xkocnv  23729  submtmd  24019  prdsdsf  24282  ressprdsds  24286  blfvalps  24298  prdsxmslem2  24444  tmsxpsval  24453  ngpds  24519  sgrimval  24547  subgngp  24550  tngngp  24569  tngngp3  24571  isnlm  24590  lssnlm  24616  isphtpy  24907  isphtpc  24920  pi1cpbl  24971  pi1addf  24974  pi1addval  24975  pi1grplem  24976  clmsub  25007  clmvsass  25016  clmvsdir  25018  isclmp  25024  cvsdiv  25059  iscph  25097  cphdir  25132  cphdi  25133  cph2di  25134  cph2subdi  25137  cphass  25138  tcphval  25145  ipcau2  25161  tcphcphlem1  25162  tcphcphlem2  25163  cphsscph  25178  caufval  25202  rrxip  25317  rrxvsca  25321  rrxplusgvscavalb  25322  rrxdsfival  25340  ehleudisval  25346  dvlip2  25927  q1pval  26087  r1pval  26090  dvntaylp  26306  efabl  26486  efsubm  26487  dchrmul  27186  seqseq123d  28216  istrkgc  28432  istrkgb  28433  istrkgcb  28434  istrkge  28435  istrkgl  28436  istrkgld  28437  iscgrg  28490  isismt  28512  tglngval  28529  legval  28562  ishlg  28580  mirval  28633  israg  28675  ishpg  28737  lmif  28763  islmib  28765  isinag  28816  ttgval  28853  wksonproplem  29681  wspthsnon  29830  iswwlksnon  29831  iswspthsnon  29834  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  33025  inftmrel  33149  isinftm  33150  isslmd  33171  elrgspnlem1  33209  erlval  33225  rlocval  33226  rlocaddval  33235  rlocmulval  33236  subrdom  33251  resv1r  33304  lsmidllsp  33365  idlinsubrg  33396  prmidlval  33402  idlsrgval  33468  idlsrg0g  33471  rprmval  33481  ressply1evls1  33528  drgextlsp  33606  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  extdg1id  33679  fldextrspunlsplem  33686  fldextrspunlsp  33687  extdgfialglem1  33705  extdgfialglem2  33706  algextdeglem8  33737  smatlem  33810  submatminr1  33823  metidval  33903  pstmval  33908  pstmfval  33909  zlm0  33973  zlm1  33974  sitmval  34362  breprexp  34646  istrkg2d  34679  afsval  34684  mclsrcl  35605  mppsval  35616  bj-endval  37359  matunitlindflem2  37656  istotbnd  37808  isbnd  37819  rrnequiv  37874  isrngo  37936  rngohomval  38003  idlval  38052  pridlval  38072  lflset  39157  islfld  39160  ldualvadd  39227  ldualsmul  39233  ldualvs  39235  isopos  39278  cmtfvalN  39308  iscvlat  39421  ishlat1  39450  lineset  39836  psubspset  39842  paddfval  39895  paddval  39896  ltrnfset  40215  trnfsetN  40253  trlfset  40258  tgrpov  40846  erngplus  40901  erngmul  40904  erngplus-rN  40909  erngmul-rN  40912  erngdvlem3  41088  erngdvlem4  41089  erng0g  41092  erngdvlem3-rN  41096  erngdvlem4-rN  41097  dvaplusg  41107  dvamulr  41110  dvavadd  41113  dvavsca  41115  dvalveclem  41123  dvhmulr  41184  dvhfvadd  41189  dvhvadd  41190  dvhopvadd2  41192  dvhvaddcl  41193  dvhvaddcomN  41194  dvhvsca  41199  dvhlveclem  41206  dvh0g  41209  djavalN  41233  diblsmopel  41269  dicvaddcl  41288  cdlemn6  41300  dihffval  41328  dihopelvalcpre  41346  djhval  41496  lcdvaddval  41696  lcdsmul  41700  lcdvsval  41702  lcdlkreq2N  41721  hvmapffval  41856  hvmapfval  41857  hdmap1fval  41894  hgmapffval  41983  hgmapfval  41984  hgmapadd  41992  hlhilipval  42047  hlhilhillem  42058  isprimroot  42185  aks6d1c1p4  42203  idomnnzpownz  42224  aks6d1c5lem1  42228  aks6d1c5lem3  42229  aks6d1c5lem2  42230  aks5lem3a  42281  unitscyglem5  42291  rhmpsr1  42645  selvvvval  42677  mhphf2  42690  prjspval  42695  prjspner1  42718  sn-isghm  42765  mnringvald  44305  ioorrnopnlem  46401  hoidmvval0b  46687  hoidmvlelem2  46693  hoidmvlelem3  46694  hoidmvle  46697  ovnhoi  46700  hoiqssbl  46722  hspmbllem2  46724  vonioo  46779  vonicc  46782  zlidlring  48333  uzlidlring  48334  ovmpordxf  48438  lincop  48508  lincval  48509  lincsum  48529  lincscm  48530  lmod1lem2  48588  lmod1lem3  48589  lmod1lem4  48590  ldepsnlinc  48608  lines  48831  line  48832  rrxlines  48833  rrxline  48834  spheres  48846  fvconstr  48961  fvconstrn0  48962  fvconstr2  48963  catprs  49111  sectrcl2  49123  invrcl2  49125  invfn  49130  isorcl2  49134  sectpropdlem  49136  invpropdlem  49138  isopropdlem  49140  cicpropdlem  49149  iinfconstbas  49166  nelsubclem  49167  nelsubc3lem  49170  ssccatid  49172  resccatlem  49173  cofu2a  49195  cofid2a  49213  cofid2  49215  cofidf2a  49217  cofidf2  49220  oppf2  49240  upfval  49276  upfval2  49277  upfval3  49278  upeu3  49295  upeu4  49296  oppcup3  49309  natoppfb  49331  swapfval  49362  swapf2a  49371  1stfpropd  49390  2ndfpropd  49391  cofuswapf2  49395  tposcurf12  49398  tposcurf2  49400  tposcurf2cl  49402  fucofvalg  49418  fuco11b  49437  fuco23a  49452  precofval3  49471  prcofpropd  49479  catcrcl2  49496  opf12  49504  fucoppcco  49509  thincmod  49530  isthincd2lem2  49535  isthincd  49536  dfinito4  49601  mndtcco2  49686  mndtccatid  49687  oppgoppchom  49690  oppgoppcco  49691  grptcmon  49693  grptcepi  49694  2arwcatlem2  49696  2arwcatlem3  49697  2arwcatlem4  49698  2arwcat  49700  lanrcl  49721  ranrcl  49722  rellan  49723  relran  49724  concom  49763  coccom  49764