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  16175  vdwapval  16920  vdwapid1  16922  vdwmc2  16926  vdwpc  16927  vdwlem5  16932  vdwlem8  16935  vdwlem13  16940  prdsval  17394  prdsdsval2  17423  pwsplusgval  17429  pwsmulrval  17430  pwsvscafval  17433  imasval  17450  iscat  17613  iscatd  17614  catidex  17615  catideu  17616  cidfval  17617  cidval  17618  catidd  17621  iscatd2  17622  catlid  17624  catrid  17625  homffval  17631  homfeqd  17636  homfeqval  17638  comfffval  17639  comffval  17640  comfeq  17647  comfeqd  17648  comfeqval  17649  catpropd  17650  oppcval  17654  oppcco  17658  monfval  17674  ismon  17675  oppcmon  17680  oppcepi  17681  sectffval  17692  sectfval  17693  invffval  17700  isoval  17707  dfiso2  17714  isofn  17717  invisoinvl  17732  invcoisoid  17734  isocoinvid  17735  issubc  17777  issubc3  17791  isfunc  17806  cofuval  17824  cofuval2  17829  funcres  17838  funcres2b  17839  funcres2  17840  idfusubc  17842  funcres2c  17845  isfull  17854  isfth  17858  fullres2c  17883  natfval  17891  isnat  17892  fucval  17903  fucco  17907  fucpropd  17922  initoval  17935  termoval  17936  homarcl  17970  coafval  18006  resssetc  18034  resscatc  18051  catciso  18053  xpcval  18118  1stfval  18132  2ndfval  18135  prfval  18140  prfcl  18144  evlfval  18158  curfval  18164  curf1cl  18169  curfcl  18173  uncf1  18177  uncf2  18178  diag12  18185  diag2  18186  curf2ndf  18188  hofval  18193  hof1  18195  hof2fval  18196  hofcl  18200  yon12  18206  yon2  18207  hofpropd  18208  joinval  18316  meetval  18330  isdlat  18463  plusffval  18555  ismgmd  18561  issstrmgm  18562  grpidval  18570  grpidd  18580  gsumvalx  18585  gsumpropd  18587  gsumress  18591  ismgmhm  18605  issubmgm  18611  resmgmhm  18620  resmgmhm2  18621  resmgmhm2b  18622  issgrpd  18639  ismndd  18665  issubmnd  18670  submnd0  18672  ismhm  18694  issubm  18712  resmhm  18729  resmhm2  18730  resmhm2b  18731  mhmimalem  18733  isgrp  18853  isgrpd2e  18869  grpidd2  18891  grpinvfval  18892  grpinvfvalALT  18893  imasgrp2  18969  imasgrp  18970  subg0  19046  subginv  19047  subgcl  19050  issubgrpd2  19056  isnsg  19069  isghm  19129  isghmOLD  19130  resghm  19146  isga  19205  subgga  19214  gasubg  19216  cntzfval  19234  resscntz  19247  odfval  19446  odfvalALT  19447  gexval  19492  lsmfval  19552  lsmvalx  19553  oppglsm  19556  subglsm  19587  pj1fval  19608  efgtval  19637  iscmn  19703  iscmnd  19708  submcmn2  19753  imasabl  19790  iscyg  19793  cycsubmcmn  19803  isomnd  20037  submomnd  20046  prdsmgp  20071  rngpropd  20094  ringurd  20105  issrg  20108  isring  20157  ringidss  20197  mulgass3  20273  dvdsrval  20281  rdivmuldivd  20333  isirred  20339  rnghmval  20360  islring  20460  lringuplu  20464  subrngmcl  20477  subrg1  20502  subrgdvds  20506  subrguss  20507  subrginv  20508  subrgdv  20509  subrgunit  20510  subrgugrp  20511  rnghmresel  20540  rngchom  20543  rngcco  20547  rnghmsubcsetclem1  20551  rhmresel  20569  ringchom  20572  ringcco  20576  rhmsubcsetclem1  20580  rhmsubcrngclem1  20586  rrgval  20617  isdrngd  20685  isdrngrd  20686  isdrngdOLD  20687  isdrngrdOLD  20688  abvfval  20730  isabvd  20732  issrngd  20775  isorng  20781  suborng  20796  islmod  20802  islmodd  20804  scaffval  20818  lmodpropd  20863  lssset  20871  islssd  20873  prdslmodd  20907  islmhm  20966  reslmhm  20991  reslmhm2  20992  reslmhm2b  20993  islbs  21015  rlmvneg  21145  rnglidlmmgm  21187  rnglidlmsgrp  21188  rnglidlrng  21189  rngqiprngghmlem3  21231  rngqiprngimfolem  21232  rngqiprnglinlem1  21233  rngqiprngimf1  21242  rngqiprnglin  21244  rng2idl1cntr  21247  rngqiprngfulem5  21257  irinitoringc  21421  isphl  21570  ipffval  21590  isphld  21596  phssipval  21599  phssip  21600  phlssphl  21601  ocvfval  21608  isobs  21662  frlmplusgval  21706  frlmsubgval  21707  frlmvscafval  21708  frlmip  21720  frlmipval  21721  frlmup1  21740  lsslindf  21772  isassa  21798  isassad  21807  sraassab  21810  assamulgscmlem2  21842  psrval  21857  resspsradd  21917  resspsrmul  21918  resspsrvsca  21919  mplmon2mul  22009  ply1coe  22218  ply1chr  22226  lply1binomsc  22231  evl1expd  22265  evl1scvarpw  22283  asclply1subcl  22294  mamufval  22312  matplusg2  22347  matvsca2  22348  matplusgcell  22353  matsubgcell  22354  matinvgcell  22355  matvscacell  22356  matmulcell  22365  mpomatmul  22366  mat1  22367  mattposm  22379  mat1dimmul  22396  dmatmul  22417  dmatcrng  22422  scmataddcl  22436  scmatsubcl  22437  scmatcrng  22441  smatvscl  22444  scmatghm  22453  scmatmhm  22454  mvmulfval  22462  ma1repveval  22491  mdetrlin  22522  mdetrsca  22523  mdetmul  22543  madurid  22564  minmar1cl  22571  smadiadetglem1  22591  smadiadetr  22595  matinv  22597  slesolinv  22600  slesolinvbi  22601  cramerimplem3  22605  cpmatacl  22636  mat2pmatghm  22650  decpmatmullem  22691  decpmatmul  22692  pmatcollpw1lem1  22694  pmatcollpw2lem  22697  pmatcollpwlem  22700  pmatcollpw3lem  22703  mply1topmatval  22724  mp2pm2mplem1  22726  mp2pm2mplem4  22729  mp2pm2mplem5  22730  mp2pm2mp  22731  chpmat1d  22756  chpscmatgsummon  22765  chfacfpmmulgsum2  22785  xkocnv  23734  submtmd  24024  prdsdsf  24288  ressprdsds  24292  blfvalps  24304  prdsxmslem2  24450  tmsxpsval  24459  ngpds  24525  sgrimval  24553  subgngp  24556  tngngp  24575  tngngp3  24577  isnlm  24596  lssnlm  24622  isphtpy  24913  isphtpc  24926  pi1cpbl  24977  pi1addf  24980  pi1addval  24981  pi1grplem  24982  clmsub  25013  clmvsass  25022  clmvsdir  25024  isclmp  25030  cvsdiv  25065  iscph  25103  cphdir  25138  cphdi  25139  cph2di  25140  cph2subdi  25143  cphass  25144  tcphval  25151  ipcau2  25167  tcphcphlem1  25168  tcphcphlem2  25169  cphsscph  25184  caufval  25208  rrxip  25323  rrxvsca  25327  rrxplusgvscavalb  25328  rrxdsfival  25346  ehleudisval  25352  dvlip2  25933  q1pval  26093  r1pval  26096  dvntaylp  26312  efabl  26492  efsubm  26493  dchrmul  27192  seqseq123d  28220  istrkgc  28434  istrkgb  28435  istrkgcb  28436  istrkge  28437  istrkgl  28438  istrkgld  28439  iscgrg  28492  isismt  28514  tglngval  28531  legval  28564  ishlg  28582  mirval  28635  israg  28677  ishpg  28739  lmif  28765  islmib  28767  isinag  28818  ttgval  28855  wksonproplem  29683  wspthsnon  29832  iswwlksnon  29833  iswspthsnon  29836  isconngr  30168  isconngr1  30169  grpodivval  30514  dipfval  30681  ipval  30682  sspgval  30708  sspsval  30710  lnoval  30731  ajfval  30788  dipdir  30821  dipass  30824  htth  30897  ressmulgnn0d  33028  inftmrel  33149  isinftm  33150  isslmd  33171  elrgspnlem1  33209  erlval  33225  rlocval  33226  rlocaddval  33235  rlocmulval  33236  subrdom  33251  resv1r  33304  lsmidllsp  33364  idlinsubrg  33395  prmidlval  33401  idlsrgval  33467  idlsrg0g  33470  rprmval  33480  ressply1evls1  33527  drgextlsp  33582  fedgmullem1  33618  fedgmullem2  33619  fedgmul  33620  extdg1id  33654  fldextrspunlsplem  33661  fldextrspunlsp  33662  algextdeglem8  33707  smatlem  33780  submatminr1  33793  metidval  33873  pstmval  33878  pstmfval  33879  zlm0  33943  zlm1  33944  sitmval  34333  breprexp  34617  istrkg2d  34650  afsval  34655  mclsrcl  35541  mppsval  35552  bj-endval  37296  matunitlindflem2  37604  istotbnd  37756  isbnd  37767  rrnequiv  37822  isrngo  37884  rngohomval  37951  idlval  38000  pridlval  38020  lflset  39045  islfld  39048  ldualvadd  39115  ldualsmul  39121  ldualvs  39123  isopos  39166  cmtfvalN  39196  iscvlat  39309  ishlat1  39338  lineset  39725  psubspset  39731  paddfval  39784  paddval  39785  ltrnfset  40104  trnfsetN  40142  trlfset  40147  tgrpov  40735  erngplus  40790  erngmul  40793  erngplus-rN  40798  erngmul-rN  40801  erngdvlem3  40977  erngdvlem4  40978  erng0g  40981  erngdvlem3-rN  40985  erngdvlem4-rN  40986  dvaplusg  40996  dvamulr  40999  dvavadd  41002  dvavsca  41004  dvalveclem  41012  dvhmulr  41073  dvhfvadd  41078  dvhvadd  41079  dvhopvadd2  41081  dvhvaddcl  41082  dvhvaddcomN  41083  dvhvsca  41088  dvhlveclem  41095  dvh0g  41098  djavalN  41122  diblsmopel  41158  dicvaddcl  41177  cdlemn6  41189  dihffval  41217  dihopelvalcpre  41235  djhval  41385  lcdvaddval  41585  lcdsmul  41589  lcdvsval  41591  lcdlkreq2N  41610  hvmapffval  41745  hvmapfval  41746  hdmap1fval  41783  hgmapffval  41872  hgmapfval  41873  hgmapadd  41881  hlhilipval  41936  hlhilhillem  41947  isprimroot  42074  aks6d1c1p4  42092  idomnnzpownz  42113  aks6d1c5lem1  42117  aks6d1c5lem3  42118  aks6d1c5lem2  42119  aks5lem3a  42170  unitscyglem5  42180  rhmpsr1  42534  selvvvval  42566  mhphf2  42579  prjspval  42584  prjspner1  42607  sn-isghm  42654  mnringvald  44195  ioorrnopnlem  46295  hoidmvval0b  46581  hoidmvlelem2  46587  hoidmvlelem3  46588  hoidmvle  46591  ovnhoi  46594  hoiqssbl  46616  hspmbllem2  46618  vonioo  46673  vonicc  46676  zlidlring  48215  uzlidlring  48216  ovmpordxf  48320  lincop  48390  lincval  48391  lincsum  48411  lincscm  48412  lmod1lem2  48470  lmod1lem3  48471  lmod1lem4  48472  ldepsnlinc  48490  lines  48713  line  48714  rrxlines  48715  rrxline  48716  spheres  48728  fvconstr  48843  fvconstrn0  48844  fvconstr2  48845  catprs  48993  sectrcl2  49005  invrcl2  49007  invfn  49012  isorcl2  49016  sectpropdlem  49018  invpropdlem  49020  isopropdlem  49022  cicpropdlem  49031  iinfconstbas  49048  nelsubclem  49049  nelsubc3lem  49052  ssccatid  49054  resccatlem  49055  cofu2a  49077  cofid2a  49095  cofid2  49097  cofidf2a  49099  cofidf2  49102  oppf2  49122  upfval  49158  upfval2  49159  upfval3  49160  upeu3  49177  upeu4  49178  oppcup3  49191  natoppfb  49213  swapfval  49244  swapf2a  49253  1stfpropd  49272  2ndfpropd  49273  cofuswapf2  49277  tposcurf12  49280  tposcurf2  49282  tposcurf2cl  49284  fucofvalg  49300  fuco11b  49319  fuco23a  49334  precofval3  49353  prcofpropd  49361  catcrcl2  49378  opf12  49386  fucoppcco  49391  thincmod  49412  isthincd2lem2  49417  isthincd  49418  dfinito4  49483  mndtcco2  49568  mndtccatid  49569  oppgoppchom  49572  oppgoppcco  49573  grptcmon  49575  grptcepi  49576  2arwcatlem2  49578  2arwcatlem3  49579  2arwcatlem4  49580  2arwcat  49582  lanrcl  49603  ranrcl  49604  rellan  49605  relran  49606  concom  49645  coccom  49646