Theorem oveqd 7381

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

Syntax hints:   → wi 4   = wceq 1542  (class class class)co 7364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-uni 4852  df-br 5087  df-iota 6452  df-fv 6504  df-ov 7367

This theorem is referenced by:  oveq123d  7385  oveqdr  7392  csbov  7409  csbov12g  7410  ovmpodxf  7514  oprssov  7533  2mpo0  7613  ofeqd  7630  mptmpoopabbrd  8030  mptmpoopabovd  8031  el2mpocsbcl  8032  fnmpoovd  8034  frecseq123  8229  ruclem1  16195  vdwapval  16941  vdwapid1  16943  vdwmc2  16947  vdwpc  16948  vdwlem5  16953  vdwlem8  16956  vdwlem13  16961  prdsval  17415  prdsdsval2  17444  pwsplusgval  17451  pwsmulrval  17452  pwsvscafval  17455  imasval  17472  iscat  17635  iscatd  17636  catidex  17637  catideu  17638  cidfval  17639  cidval  17640  catidd  17643  iscatd2  17644  catlid  17646  catrid  17647  homffval  17653  homfeqd  17658  homfeqval  17660  comfffval  17661  comffval  17662  comfeq  17669  comfeqd  17670  comfeqval  17671  catpropd  17672  oppcval  17676  oppcco  17680  monfval  17696  ismon  17697  oppcmon  17702  oppcepi  17703  sectffval  17714  sectfval  17715  invffval  17722  isoval  17729  dfiso2  17736  isofn  17739  invisoinvl  17754  invcoisoid  17756  isocoinvid  17757  issubc  17799  issubc3  17813  isfunc  17828  cofuval  17846  cofuval2  17851  funcres  17860  funcres2b  17861  funcres2  17862  idfusubc  17864  funcres2c  17867  isfull  17876  isfth  17880  fullres2c  17905  natfval  17913  isnat  17914  fucval  17925  fucco  17929  fucpropd  17944  initoval  17957  termoval  17958  homarcl  17992  coafval  18028  resssetc  18056  resscatc  18073  catciso  18075  xpcval  18140  1stfval  18154  2ndfval  18157  prfval  18162  prfcl  18166  evlfval  18180  curfval  18186  curf1cl  18191  curfcl  18195  uncf1  18199  uncf2  18200  diag12  18207  diag2  18208  curf2ndf  18210  hofval  18215  hof1  18217  hof2fval  18218  hofcl  18222  yon12  18228  yon2  18229  hofpropd  18230  joinval  18338  meetval  18352  isdlat  18485  plusffval  18611  ismgmd  18617  issstrmgm  18618  grpidval  18626  grpidd  18636  gsumvalx  18641  gsumpropd  18643  gsumress  18647  ismgmhm  18661  issubmgm  18667  resmgmhm  18676  resmgmhm2  18677  resmgmhm2b  18678  issgrpd  18695  ismndd  18721  issubmnd  18726  submnd0  18728  ismhm  18750  issubm  18768  resmhm  18785  resmhm2  18786  resmhm2b  18787  mhmimalem  18789  isgrp  18912  isgrpd2e  18928  grpidd2  18950  grpinvfval  18951  grpinvfvalALT  18952  imasgrp2  19028  imasgrp  19029  subg0  19105  subginv  19106  subgcl  19109  issubgrpd2  19115  isnsg  19127  isghm  19187  isghmOLD  19188  resghm  19204  isga  19263  subgga  19272  gasubg  19274  cntzfval  19292  resscntz  19305  odfval  19504  odfvalALT  19505  gexval  19550  lsmfval  19610  lsmvalx  19611  oppglsm  19614  subglsm  19645  pj1fval  19666  efgtval  19695  iscmn  19761  iscmnd  19766  submcmn2  19811  imasabl  19848  iscyg  19851  cycsubmcmn  19861  isomnd  20095  submomnd  20104  prdsmgp  20129  rngpropd  20152  ringurd  20163  issrg  20166  isring  20215  ringidss  20255  mulgass3  20330  dvdsrval  20338  rdivmuldivd  20390  isirred  20396  rnghmval  20417  islring  20514  lringuplu  20518  subrngmcl  20531  subrg1  20556  subrgdvds  20560  subrguss  20561  subrginv  20562  subrgdv  20563  subrgunit  20564  subrgugrp  20565  rnghmresel  20594  rngchom  20597  rngcco  20601  rnghmsubcsetclem1  20605  rhmresel  20623  ringchom  20626  ringcco  20630  rhmsubcsetclem1  20634  rhmsubcrngclem1  20640  rrgval  20671  isdrngd  20739  isdrngrd  20740  isdrngdOLD  20741  isdrngrdOLD  20742  abvfval  20784  isabvd  20786  issrngd  20829  isorng  20835  suborng  20850  islmod  20856  islmodd  20858  scaffval  20872  lmodpropd  20917  lssset  20925  islssd  20927  prdslmodd  20961  islmhm  21020  reslmhm  21045  reslmhm2  21046  reslmhm2b  21047  islbs  21069  rlmvneg  21199  rnglidlmmgm  21241  rnglidlmsgrp  21242  rnglidlrng  21243  rngqiprngghmlem3  21285  rngqiprngimfolem  21286  rngqiprnglinlem1  21287  rngqiprngimf1  21296  rngqiprnglin  21298  rng2idl1cntr  21301  rngqiprngfulem5  21311  irinitoringc  21475  isphl  21624  ipffval  21644  isphld  21650  phssipval  21653  phssip  21654  phlssphl  21655  ocvfval  21662  isobs  21716  frlmplusgval  21760  frlmsubgval  21761  frlmvscafval  21762  frlmip  21774  frlmipval  21775  frlmup1  21794  lsslindf  21826  isassa  21852  isassad  21861  sraassab  21864  assamulgscmlem2  21896  psrval  21911  resspsradd  21969  resspsrmul  21970  resspsrvsca  21971  mplmon2mul  22063  ply1coe  22279  ply1chr  22287  lply1binomsc  22292  evl1expd  22326  evl1scvarpw  22344  asclply1subcl  22355  mamufval  22373  matplusg2  22408  matvsca2  22409  matplusgcell  22414  matsubgcell  22415  matinvgcell  22416  matvscacell  22417  matmulcell  22426  mpomatmul  22427  mat1  22428  mattposm  22440  mat1dimmul  22457  dmatmul  22478  dmatcrng  22483  scmataddcl  22497  scmatsubcl  22498  scmatcrng  22502  smatvscl  22505  scmatghm  22514  scmatmhm  22515  mvmulfval  22523  ma1repveval  22552  mdetrlin  22583  mdetrsca  22584  mdetmul  22604  madurid  22625  minmar1cl  22632  smadiadetglem1  22652  smadiadetr  22656  matinv  22658  slesolinv  22661  slesolinvbi  22662  cramerimplem3  22666  cpmatacl  22697  mat2pmatghm  22711  decpmatmullem  22752  decpmatmul  22753  pmatcollpw1lem1  22755  pmatcollpw2lem  22758  pmatcollpwlem  22761  pmatcollpw3lem  22764  mply1topmatval  22785  mp2pm2mplem1  22787  mp2pm2mplem4  22790  mp2pm2mplem5  22791  mp2pm2mp  22792  chpmat1d  22817  chpscmatgsummon  22826  chfacfpmmulgsum2  22846  xkocnv  23795  submtmd  24085  prdsdsf  24348  ressprdsds  24352  blfvalps  24364  prdsxmslem2  24510  tmsxpsval  24519  ngpds  24585  sgrimval  24613  subgngp  24616  tngngp  24635  tngngp3  24637  isnlm  24656  lssnlm  24682  isphtpy  24964  isphtpc  24977  pi1cpbl  25027  pi1addf  25030  pi1addval  25031  pi1grplem  25032  clmsub  25063  clmvsass  25072  clmvsdir  25074  isclmp  25080  cvsdiv  25115  iscph  25153  cphdir  25188  cphdi  25189  cph2di  25190  cph2subdi  25193  cphass  25194  tcphval  25201  ipcau2  25217  tcphcphlem1  25218  tcphcphlem2  25219  cphsscph  25234  caufval  25258  rrxip  25373  rrxvsca  25377  rrxplusgvscavalb  25378  rrxdsfival  25396  ehleudisval  25402  dvlip2  25978  q1pval  26136  r1pval  26139  dvntaylp  26354  efabl  26533  efsubm  26534  dchrmul  27231  seqseq123d  28298  istrkgc  28542  istrkgb  28543  istrkgcb  28544  istrkge  28545  istrkgl  28546  istrkgld  28547  iscgrg  28600  isismt  28622  tglngval  28639  legval  28672  ishlg  28690  mirval  28743  israg  28785  ishpg  28847  lmif  28873  islmib  28875  isinag  28926  ttgval  28963  wksonproplem  29792  wspthsnon  29941  iswwlksnon  29942  iswspthsnon  29945  isconngr  30280  isconngr1  30281  grpodivval  30627  dipfval  30794  ipval  30795  sspgval  30821  sspsval  30823  lnoval  30844  ajfval  30901  dipdir  30934  dipass  30937  htth  31010  ressmulgnn0d  33126  inftmrel  33262  isinftm  33263  isslmd  33284  elrgspnlem1  33324  erlval  33340  rlocval  33341  rlocaddval  33350  rlocmulval  33351  subrdom  33367  resv1r  33420  lsmidllsp  33481  idlinsubrg  33512  prmidlval  33518  idlsrgval  33584  idlsrg0g  33587  rprmval  33597  ressply1evls1  33646  vietalem  33744  drgextlsp  33759  fedgmullem1  33795  fedgmullem2  33796  fedgmul  33797  extdg1id  33832  fldextrspunlsplem  33839  fldextrspunlsp  33840  extdgfialglem1  33858  extdgfialglem2  33859  algextdeglem8  33890  smatlem  33963  submatminr1  33976  metidval  34056  pstmval  34061  pstmfval  34062  zlm0  34126  zlm1  34127  sitmval  34515  breprexp  34799  istrkg2d  34832  afsval  34837  mclsrcl  35765  mppsval  35776  bj-endval  37651  matunitlindflem2  37960  istotbnd  38112  isbnd  38123  rrnequiv  38178  isrngo  38240  rngohomval  38307  idlval  38356  pridlval  38376  lflset  39527  islfld  39530  ldualvadd  39597  ldualsmul  39603  ldualvs  39605  isopos  39648  cmtfvalN  39678  iscvlat  39791  ishlat1  39820  lineset  40206  psubspset  40212  paddfval  40265  paddval  40266  ltrnfset  40585  trnfsetN  40623  trlfset  40628  tgrpov  41216  erngplus  41271  erngmul  41274  erngplus-rN  41279  erngmul-rN  41282  erngdvlem3  41458  erngdvlem4  41459  erng0g  41462  erngdvlem3-rN  41466  erngdvlem4-rN  41467  dvaplusg  41477  dvamulr  41480  dvavadd  41483  dvavsca  41485  dvalveclem  41493  dvhmulr  41554  dvhfvadd  41559  dvhvadd  41560  dvhopvadd2  41562  dvhvaddcl  41563  dvhvaddcomN  41564  dvhvsca  41569  dvhlveclem  41576  dvh0g  41579  djavalN  41603  diblsmopel  41639  dicvaddcl  41658  cdlemn6  41670  dihffval  41698  dihopelvalcpre  41716  djhval  41866  lcdvaddval  42066  lcdsmul  42070  lcdvsval  42072  lcdlkreq2N  42091  hvmapffval  42226  hvmapfval  42227  hdmap1fval  42264  hgmapffval  42353  hgmapfval  42354  hgmapadd  42362  hlhilipval  42417  hlhilhillem  42428  isprimroot  42554  aks6d1c1p4  42572  idomnnzpownz  42593  aks6d1c5lem1  42597  aks6d1c5lem3  42598  aks6d1c5lem2  42599  aks5lem3a  42650  unitscyglem5  42660  rhmpsr1  43018  selvvvval  43040  mhphf2  43053  prjspval  43058  prjspner1  43081  sn-isghm  43128  mnringvald  44666  ioorrnopnlem  46758  hoidmvval0b  47044  hoidmvlelem2  47050  hoidmvlelem3  47051  hoidmvle  47054  ovnhoi  47057  hoiqssbl  47079  hspmbllem2  47081  vonioo  47136  vonicc  47139  zlidlring  48730  uzlidlring  48731  ovmpordxf  48835  lincop  48904  lincval  48905  lincsum  48925  lincscm  48926  lmod1lem2  48984  lmod1lem3  48985  lmod1lem4  48986  ldepsnlinc  49004  lines  49227  line  49228  rrxlines  49229  rrxline  49230  spheres  49242  fvconstr  49357  fvconstrn0  49358  fvconstr2  49359  catprs  49506  sectrcl2  49518  invrcl2  49520  invfn  49525  isorcl2  49529  sectpropdlem  49531  invpropdlem  49533  isopropdlem  49535  cicpropdlem  49544  iinfconstbas  49561  nelsubclem  49562  nelsubc3lem  49565  ssccatid  49567  resccatlem  49568  cofu2a  49590  cofid2a  49608  cofid2  49610  cofidf2a  49612  cofidf2  49615  oppf2  49635  upfval  49671  upfval2  49672  upfval3  49673  upeu3  49690  upeu4  49691  oppcup3  49704  natoppfb  49726  swapfval  49757  swapf2a  49766  1stfpropd  49785  2ndfpropd  49786  cofuswapf2  49790  tposcurf12  49793  tposcurf2  49795  tposcurf2cl  49797  fucofvalg  49813  fuco11b  49832  fuco23a  49847  precofval3  49866  prcofpropd  49874  catcrcl2  49891  opf12  49899  fucoppcco  49904  thincmod  49925  isthincd2lem2  49930  isthincd  49931  dfinito4  49996  mndtcco2  50081  mndtccatid  50082  oppgoppchom  50085  oppgoppcco  50086  grptcmon  50088  grptcepi  50089  2arwcatlem2  50091  2arwcatlem3  50092  2arwcatlem4  50093  2arwcat  50095  lanrcl  50116  ranrcl  50117  rellan  50118  relran  50119  concom  50158  coccom  50159