Theorem oveqd 7373

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3429  df-ss 3902  df-uni 4841  df-br 5075  df-iota 6443  df-fv 6495  df-ov 7359

This theorem is referenced by:  oveq123d  7377  oveqdr  7384  csbov  7401  csbov12g  7402  ovmpodxf  7506  oprssov  7525  2mpo0  7605  ofeqd  7622  mptmpoopabbrd  8022  mptmpoopabovd  8023  el2mpocsbcl  8024  fnmpoovd  8026  frecseq123  8221  ruclem1  16187  vdwapval  16933  vdwapid1  16935  vdwmc2  16939  vdwpc  16940  vdwlem5  16945  vdwlem8  16948  vdwlem13  16953  prdsval  17407  prdsdsval2  17436  pwsplusgval  17443  pwsmulrval  17444  pwsvscafval  17447  imasval  17464  iscat  17627  iscatd  17628  catidex  17629  catideu  17630  cidfval  17631  cidval  17632  catidd  17635  iscatd2  17636  catlid  17638  catrid  17639  homffval  17645  homfeqd  17650  homfeqval  17652  comfffval  17653  comffval  17654  comfeq  17661  comfeqd  17662  comfeqval  17663  catpropd  17664  oppcval  17668  oppcco  17672  monfval  17688  ismon  17689  oppcmon  17694  oppcepi  17695  sectffval  17706  sectfval  17707  invffval  17714  isoval  17721  dfiso2  17728  isofn  17731  invisoinvl  17746  invcoisoid  17748  isocoinvid  17749  issubc  17791  issubc3  17805  isfunc  17820  cofuval  17838  cofuval2  17843  funcres  17852  funcres2b  17853  funcres2  17854  idfusubc  17856  funcres2c  17859  isfull  17868  isfth  17872  fullres2c  17897  natfval  17905  isnat  17906  fucval  17917  fucco  17921  fucpropd  17936  initoval  17949  termoval  17950  homarcl  17984  coafval  18020  resssetc  18048  resscatc  18065  catciso  18067  xpcval  18132  1stfval  18146  2ndfval  18149  prfval  18154  prfcl  18158  evlfval  18172  curfval  18178  curf1cl  18183  curfcl  18187  uncf1  18191  uncf2  18192  diag12  18199  diag2  18200  curf2ndf  18202  hofval  18207  hof1  18209  hof2fval  18210  hofcl  18214  yon12  18220  yon2  18221  hofpropd  18222  joinval  18330  meetval  18344  isdlat  18477  plusffval  18603  ismgmd  18609  issstrmgm  18610  grpidval  18618  grpidd  18628  gsumvalx  18633  gsumpropd  18635  gsumress  18639  ismgmhm  18653  issubmgm  18659  resmgmhm  18668  resmgmhm2  18669  resmgmhm2b  18670  issgrpd  18687  ismndd  18713  issubmnd  18718  submnd0  18720  ismhm  18742  issubm  18760  resmhm  18777  resmhm2  18778  resmhm2b  18779  mhmimalem  18781  isgrp  18904  isgrpd2e  18920  grpidd2  18942  grpinvfval  18943  grpinvfvalALT  18944  imasgrp2  19020  imasgrp  19021  subg0  19097  subginv  19098  subgcl  19101  issubgrpd2  19107  isnsg  19119  isghm  19179  isghmOLD  19180  resghm  19196  isga  19255  subgga  19264  gasubg  19266  cntzfval  19284  resscntz  19297  odfval  19496  odfvalALT  19497  gexval  19542  lsmfval  19602  lsmvalx  19603  oppglsm  19606  subglsm  19637  pj1fval  19658  efgtval  19687  iscmn  19753  iscmnd  19758  submcmn2  19803  imasabl  19840  iscyg  19843  cycsubmcmn  19853  isomnd  20087  submomnd  20096  prdsmgp  20121  rngpropd  20144  ringurd  20155  issrg  20158  isring  20207  ringidss  20247  mulgass3  20322  dvdsrval  20330  rdivmuldivd  20382  isirred  20388  rnghmval  20409  islring  20506  lringuplu  20510  subrngmcl  20523  subrg1  20548  subrgdvds  20552  subrguss  20553  subrginv  20554  subrgdv  20555  subrgunit  20556  subrgugrp  20557  rnghmresel  20586  rngchom  20589  rngcco  20593  rnghmsubcsetclem1  20597  rhmresel  20615  ringchom  20618  ringcco  20622  rhmsubcsetclem1  20626  rhmsubcrngclem1  20632  rrgval  20663  isdrngd  20731  isdrngrd  20732  isdrngdOLD  20733  isdrngrdOLD  20734  abvfval  20776  isabvd  20778  issrngd  20821  isorng  20827  suborng  20842  islmod  20848  islmodd  20850  scaffval  20864  lmodpropd  20909  lssset  20917  islssd  20919  prdslmodd  20953  islmhm  21011  reslmhm  21036  reslmhm2  21037  reslmhm2b  21038  islbs  21060  rlmvneg  21190  rnglidlmmgm  21232  rnglidlmsgrp  21233  rnglidlrng  21234  rngqiprngghmlem3  21276  rngqiprngimfolem  21277  rngqiprnglinlem1  21278  rngqiprngimf1  21287  rngqiprnglin  21289  rng2idl1cntr  21292  rngqiprngfulem5  21302  irinitoringc  21448  isphl  21597  ipffval  21617  isphld  21623  phssipval  21626  phssip  21627  phlssphl  21628  ocvfval  21635  isobs  21689  frlmplusgval  21733  frlmsubgval  21734  frlmvscafval  21735  frlmip  21747  frlmipval  21748  frlmup1  21767  lsslindf  21799  isassa  21825  isassad  21834  sraassab  21837  assamulgscmlem2  21869  psrval  21884  resspsradd  21942  resspsrmul  21943  resspsrvsca  21944  mplmon2mul  22036  ply1coe  22251  ply1chr  22259  lply1binomsc  22264  evl1expd  22298  evl1scvarpw  22316  asclply1subcl  22327  mamufval  22345  matplusg2  22380  matvsca2  22381  matplusgcell  22386  matsubgcell  22387  matinvgcell  22388  matvscacell  22389  matmulcell  22398  mpomatmul  22399  mat1  22400  mattposm  22412  mat1dimmul  22429  dmatmul  22450  dmatcrng  22455  scmataddcl  22469  scmatsubcl  22470  scmatcrng  22474  smatvscl  22477  scmatghm  22486  scmatmhm  22487  mvmulfval  22495  ma1repveval  22524  mdetrlin  22555  mdetrsca  22556  mdetmul  22576  madurid  22597  minmar1cl  22604  smadiadetglem1  22624  smadiadetr  22628  matinv  22630  slesolinv  22633  slesolinvbi  22634  cramerimplem3  22638  cpmatacl  22669  mat2pmatghm  22683  decpmatmullem  22724  decpmatmul  22725  pmatcollpw1lem1  22727  pmatcollpw2lem  22730  pmatcollpwlem  22733  pmatcollpw3lem  22736  mply1topmatval  22757  mp2pm2mplem1  22759  mp2pm2mplem4  22762  mp2pm2mplem5  22763  mp2pm2mp  22764  chpmat1d  22789  chpscmatgsummon  22798  chfacfpmmulgsum2  22818  xkocnv  23767  submtmd  24057  prdsdsf  24320  ressprdsds  24324  blfvalps  24336  prdsxmslem2  24482  tmsxpsval  24491  ngpds  24557  sgrimval  24585  subgngp  24588  tngngp  24607  tngngp3  24609  isnlm  24628  lssnlm  24654  isphtpy  24936  isphtpc  24949  pi1cpbl  24999  pi1addf  25002  pi1addval  25003  pi1grplem  25004  clmsub  25035  clmvsass  25044  clmvsdir  25046  isclmp  25052  cvsdiv  25087  iscph  25125  cphdir  25160  cphdi  25161  cph2di  25162  cph2subdi  25165  cphass  25166  tcphval  25173  ipcau2  25189  tcphcphlem1  25190  tcphcphlem2  25191  cphsscph  25206  caufval  25230  rrxip  25345  rrxvsca  25349  rrxplusgvscavalb  25350  rrxdsfival  25368  ehleudisval  25374  dvlip2  25950  q1pval  26108  r1pval  26111  dvntaylp  26324  efabl  26502  efsubm  26503  dchrmul  27199  seqseq123d  28266  istrkgc  28510  istrkgb  28511  istrkgcb  28512  istrkge  28513  istrkgl  28514  istrkgld  28515  iscgrg  28568  isismt  28590  tglngval  28607  legval  28640  ishlg  28658  mirval  28711  israg  28753  ishpg  28815  lmif  28841  islmib  28843  isinag  28894  ttgval  28931  wksonproplem  29759  wspthsnon  29908  iswwlksnon  29909  iswspthsnon  29912  isconngr  30247  isconngr1  30248  grpodivval  30594  dipfval  30761  ipval  30762  sspgval  30788  sspsval  30790  lnoval  30811  ajfval  30868  dipdir  30901  dipass  30904  htth  30977  ressmulgnn0d  33093  inftmrel  33229  isinftm  33230  isslmd  33251  elrgspnlem1  33291  erlval  33307  rlocval  33308  rlocaddval  33317  rlocmulval  33318  subrdom  33334  resv1r  33387  lsmidllsp  33448  idlinsubrg  33479  prmidlval  33485  idlsrgval  33551  idlsrg0g  33554  rprmval  33564  ressply1evls1  33613  vietalem  33711  drgextlsp  33726  fedgmullem1  33761  fedgmullem2  33762  fedgmul  33763  extdg1id  33798  fldextrspunlsplem  33805  fldextrspunlsp  33806  extdgfialglem1  33824  extdgfialglem2  33825  algextdeglem8  33856  smatlem  33929  submatminr1  33942  metidval  34022  pstmval  34027  pstmfval  34028  zlm0  34092  zlm1  34093  sitmval  34481  breprexp  34765  istrkg2d  34798  afsval  34803  mclsrcl  35731  mppsval  35742  bj-endval  37617  matunitlindflem2  37926  istotbnd  38078  isbnd  38089  rrnequiv  38144  isrngo  38206  rngohomval  38273  idlval  38322  pridlval  38342  lflset  39493  islfld  39496  ldualvadd  39563  ldualsmul  39569  ldualvs  39571  isopos  39614  cmtfvalN  39644  iscvlat  39757  ishlat1  39786  lineset  40172  psubspset  40178  paddfval  40231  paddval  40232  ltrnfset  40551  trnfsetN  40589  trlfset  40594  tgrpov  41182  erngplus  41237  erngmul  41240  erngplus-rN  41245  erngmul-rN  41248  erngdvlem3  41424  erngdvlem4  41425  erng0g  41428  erngdvlem3-rN  41432  erngdvlem4-rN  41433  dvaplusg  41443  dvamulr  41446  dvavadd  41449  dvavsca  41451  dvalveclem  41459  dvhmulr  41520  dvhfvadd  41525  dvhvadd  41526  dvhopvadd2  41528  dvhvaddcl  41529  dvhvaddcomN  41530  dvhvsca  41535  dvhlveclem  41542  dvh0g  41545  djavalN  41569  diblsmopel  41605  dicvaddcl  41624  cdlemn6  41636  dihffval  41664  dihopelvalcpre  41682  djhval  41832  lcdvaddval  42032  lcdsmul  42036  lcdvsval  42038  lcdlkreq2N  42057  hvmapffval  42192  hvmapfval  42193  hdmap1fval  42230  hgmapffval  42319  hgmapfval  42320  hgmapadd  42328  hlhilipval  42383  hlhilhillem  42394  isprimroot  42520  aks6d1c1p4  42538  idomnnzpownz  42559  aks6d1c5lem1  42563  aks6d1c5lem3  42564  aks6d1c5lem2  42565  aks5lem3a  42616  unitscyglem5  42626  rhmpsr1  42984  selvvvval  43006  mhphf2  43019  prjspval  43024  prjspner1  43047  sn-isghm  43094  mnringvald  44628  ioorrnopnlem  46720  hoidmvval0b  47006  hoidmvlelem2  47012  hoidmvlelem3  47013  hoidmvle  47016  ovnhoi  47019  hoiqssbl  47041  hspmbllem2  47043  vonioo  47098  vonicc  47101  zlidlring  48698  uzlidlring  48699  ovmpordxf  48803  lincop  48872  lincval  48873  lincsum  48893  lincscm  48894  lmod1lem2  48952  lmod1lem3  48953  lmod1lem4  48954  ldepsnlinc  48972  lines  49195  line  49196  rrxlines  49197  rrxline  49198  spheres  49210  fvconstr  49325  fvconstrn0  49326  fvconstr2  49327  catprs  49474  sectrcl2  49486  invrcl2  49488  invfn  49493  isorcl2  49497  sectpropdlem  49499  invpropdlem  49501  isopropdlem  49503  cicpropdlem  49512  iinfconstbas  49529  nelsubclem  49530  nelsubc3lem  49533  ssccatid  49535  resccatlem  49536  cofu2a  49558  cofid2a  49576  cofid2  49578  cofidf2a  49580  cofidf2  49583  oppf2  49603  upfval  49639  upfval2  49640  upfval3  49641  upeu3  49658  upeu4  49659  oppcup3  49672  natoppfb  49694  swapfval  49725  swapf2a  49734  1stfpropd  49753  2ndfpropd  49754  cofuswapf2  49758  tposcurf12  49761  tposcurf2  49763  tposcurf2cl  49765  fucofvalg  49781  fuco11b  49800  fuco23a  49815  precofval3  49834  prcofpropd  49842  catcrcl2  49859  opf12  49867  fucoppcco  49872  thincmod  49893  isthincd2lem2  49898  isthincd  49899  dfinito4  49964  mndtcco2  50049  mndtccatid  50050  oppgoppchom  50053  oppgoppcco  50054  grptcmon  50056  grptcepi  50057  2arwcatlem2  50059  2arwcatlem3  50060  2arwcatlem4  50061  2arwcat  50063  lanrcl  50084  ranrcl  50085  rellan  50086  relran  50087  concom  50126  coccom  50127