Theorem oveqd 7301

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

Syntax hints:   → wi 4   = wceq 1539  (class class class)co 7284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287

This theorem is referenced by:  oveq123d  7305  oveqdr  7312  csbov  7327  csbov12g  7328  ovmpodxf  7432  oprssov  7450  2mpo0  7527  ofeqd  7544  mptmpoopabbrd  7930  mptmpoopabovd  7931  mptmpoopabbrdOLD  7932  mptmpoopabovdOLD  7933  el2mpocsbcl  7934  fnmpoovd  7936  frecseq123  8107  ruclem1  15949  vdwapval  16683  vdwapid1  16685  vdwmc2  16689  vdwpc  16690  vdwlem5  16695  vdwlem8  16698  vdwlem13  16703  prdsval  17175  prdsdsval2  17204  pwsplusgval  17210  pwsmulrval  17211  pwsvscafval  17214  imasval  17231  iscat  17390  iscatd  17391  catidex  17392  catideu  17393  cidfval  17394  cidval  17395  catidd  17398  iscatd2  17399  catlid  17401  catrid  17402  homffval  17408  homfeqd  17413  homfeqval  17415  comfffval  17416  comffval  17417  comfeq  17424  comfeqd  17425  comfeqval  17426  catpropd  17427  oppcval  17431  oppcco  17436  monfval  17453  ismon  17454  oppcmon  17459  oppcepi  17460  sectffval  17471  sectfval  17472  invffval  17479  isoval  17486  dfiso2  17493  isofn  17496  invisoinvl  17511  invcoisoid  17513  isocoinvid  17514  issubc  17559  issubc3  17573  isfunc  17588  cofuval  17606  cofuval2  17611  funcres  17620  funcres2b  17621  funcres2  17622  funcres2c  17626  isfull  17635  isfth  17639  fullres2c  17664  natfval  17671  isnat  17672  fucval  17684  fucco  17689  fucpropd  17704  initoval  17717  termoval  17718  homarcl  17752  coafval  17788  resssetc  17816  resscatc  17833  catciso  17835  xpcval  17903  1stfval  17917  2ndfval  17920  prfval  17925  prfcl  17929  evlfval  17944  curfval  17950  curf1cl  17955  curfcl  17959  uncf1  17963  uncf2  17964  diag12  17971  diag2  17972  curf2ndf  17974  hofval  17979  hof1  17981  hof2fval  17982  hofcl  17986  yon12  17992  yon2  17993  hofpropd  17994  joinval  18104  meetval  18118  isdlat  18249  plusffval  18341  issstrmgm  18346  grpidval  18354  grpidd  18364  gsumvalx  18369  gsumpropd  18371  gsumress  18375  ismndd  18416  issubmnd  18421  submnd0  18423  ismhm  18441  issubm  18451  resmhm  18468  resmhm2  18469  resmhm2b  18470  isgrp  18592  isgrpd2e  18607  grpidd2  18626  grpinvfval  18627  grpinvfvalALT  18628  imasgrp2  18699  imasgrp  18700  subg0  18770  subginv  18771  subgcl  18774  issubgrpd2  18780  isnsg  18792  isghm  18843  resghm  18859  isga  18906  subgga  18915  gasubg  18917  cntzfval  18935  resscntz  18947  odfval  19149  odfvalALT  19150  gexval  19192  lsmfval  19252  lsmvalx  19253  oppglsm  19256  subglsm  19288  pj1fval  19309  efgtval  19338  iscmn  19403  iscmnd  19408  submcmn2  19449  iscyg  19488  cycsubmcmn  19498  issrg  19752  isring  19796  ringidss  19825  prdsmgp  19858  mulgass3  19888  dvdsrval  19896  isirred  19950  isdrngd  20025  isdrngrd  20026  subrg1  20043  subrgmcl  20045  subrgdvds  20047  subrguss  20048  subrginv  20049  subrgdv  20050  subrgunit  20051  subrgugrp  20052  abvfval  20087  isabvd  20089  issrngd  20130  islmod  20136  islmodd  20138  scaffval  20150  lmodpropd  20195  lssset  20204  islssd  20206  prdslmodd  20240  islmhm  20298  reslmhm  20323  reslmhm2  20324  reslmhm2b  20325  islbs  20347  rlmvneg  20487  rrgval  20567  isphl  20842  ipffval  20862  isphld  20868  phssipval  20871  phssip  20872  phlssphl  20873  ocvfval  20880  isobs  20936  frlmplusgval  20980  frlmsubgval  20981  frlmvscafval  20982  frlmip  20994  frlmipval  20995  frlmup1  21014  lsslindf  21046  isassa  21072  isassad  21080  assamulgscmlem2  21113  psrval  21127  resspsradd  21194  resspsrmul  21195  resspsrvsca  21196  mplmon2mul  21286  ply1coe  21476  lply1binomsc  21487  evl1expd  21520  evl1scvarpw  21538  mamufval  21543  matplusg2  21585  matvsca2  21586  matplusgcell  21591  matsubgcell  21592  matinvgcell  21593  matvscacell  21594  matmulcell  21603  mpomatmul  21604  mat1  21605  mattposm  21617  mat1dimmul  21634  dmatmul  21655  dmatcrng  21660  scmataddcl  21674  scmatsubcl  21675  scmatcrng  21679  smatvscl  21682  scmatghm  21691  scmatmhm  21692  mvmulfval  21700  ma1repveval  21729  mdetrlin  21760  mdetrsca  21761  mdetmul  21781  madurid  21802  minmar1cl  21809  smadiadetglem1  21829  smadiadetr  21833  matinv  21835  slesolinv  21838  slesolinvbi  21839  cramerimplem3  21843  cpmatacl  21874  mat2pmatghm  21888  decpmatmullem  21929  decpmatmul  21930  pmatcollpw1lem1  21932  pmatcollpw2lem  21935  pmatcollpwlem  21938  pmatcollpw3lem  21941  mply1topmatval  21962  mp2pm2mplem1  21964  mp2pm2mplem4  21967  mp2pm2mplem5  21968  mp2pm2mp  21969  chpmat1d  21994  chpscmatgsummon  22003  chfacfpmmulgsum2  22023  xkocnv  22974  submtmd  23264  prdsdsf  23529  ressprdsds  23533  blfvalps  23545  prdsxmslem2  23694  tmsxpsval  23703  ngpds  23769  sgrimval  23797  subgngp  23800  tngngp  23827  tngngp3  23829  isnlm  23848  lssnlm  23874  isphtpy  24153  isphtpc  24166  pi1cpbl  24216  pi1addf  24219  pi1addval  24220  pi1grplem  24221  clmsub  24252  clmvsass  24261  clmvsdir  24263  isclmp  24269  cvsdiv  24304  iscph  24343  cphdir  24378  cphdi  24379  cph2di  24380  cph2subdi  24383  cphass  24384  tcphval  24391  ipcau2  24407  tcphcphlem1  24408  tcphcphlem2  24409  cphsscph  24424  caufval  24448  rrxip  24563  rrxvsca  24567  rrxplusgvscavalb  24568  rrxdsfival  24586  ehleudisval  24592  dvlip2  25168  q1pval  25327  r1pval  25330  dvntaylp  25539  efabl  25715  efsubm  25716  dchrmul  26405  istrkgc  26824  istrkgb  26825  istrkgcb  26826  istrkge  26827  istrkgl  26828  istrkgld  26829  iscgrg  26882  isismt  26904  tglngval  26921  legval  26954  ishlg  26972  mirval  27025  israg  27067  ishpg  27129  lmif  27155  islmib  27157  isinag  27208  ttgval  27245  ttgvalOLD  27246  wksonproplem  28081  wksonproplemOLD  28082  wspthsnon  28226  iswwlksnon  28227  iswspthsnon  28230  isconngr  28562  isconngr1  28563  grpodivval  28906  dipfval  29073  ipval  29074  sspgval  29100  sspsval  29102  lnoval  29123  ajfval  29180  dipdir  29213  dipass  29216  htth  29289  isomnd  31336  submomnd  31345  inftmrel  31443  isinftm  31444  isslmd  31464  rngurd  31491  rdivmuldivd  31497  isorng  31507  suborng  31523  resv1r  31550  lsmidllsp  31597  idlinsubrg  31617  prmidlval  31621  idlsrgval  31657  idlsrg0g  31660  rprmval  31673  ply1chr  31678  drgextlsp  31690  fedgmullem1  31719  fedgmullem2  31720  fedgmul  31721  extdg1id  31747  smatlem  31756  submatminr1  31769  metidval  31849  pstmval  31854  pstmfval  31855  zlm0  31919  zlm1  31920  sitmval  32325  breprexp  32622  istrkg2d  32655  afsval  32660  mclsrcl  33532  mppsval  33543  bj-endval  35495  matunitlindflem2  35783  istotbnd  35936  isbnd  35947  rrnequiv  36002  isrngo  36064  rngohomval  36131  idlval  36180  pridlval  36200  lflset  37080  islfld  37083  ldualvadd  37150  ldualsmul  37156  ldualvs  37158  isopos  37201  cmtfvalN  37231  iscvlat  37344  ishlat1  37373  lineset  37759  psubspset  37765  paddfval  37818  paddval  37819  ltrnfset  38138  trnfsetN  38176  trlfset  38181  tgrpov  38769  erngplus  38824  erngmul  38827  erngplus-rN  38832  erngmul-rN  38835  erngdvlem3  39011  erngdvlem4  39012  erng0g  39015  erngdvlem3-rN  39019  erngdvlem4-rN  39020  dvaplusg  39030  dvamulr  39033  dvavadd  39036  dvavsca  39038  dvalveclem  39046  dvhmulr  39107  dvhfvadd  39112  dvhvadd  39113  dvhopvadd2  39115  dvhvaddcl  39116  dvhvaddcomN  39117  dvhvsca  39122  dvhlveclem  39129  dvh0g  39132  djavalN  39156  diblsmopel  39192  dicvaddcl  39211  cdlemn6  39223  dihffval  39251  dihopelvalcpre  39269  djhval  39419  lcdvaddval  39619  lcdsmul  39623  lcdvsval  39625  lcdlkreq2N  39644  hvmapffval  39779  hvmapfval  39780  hdmap1fval  39817  hgmapffval  39906  hgmapfval  39907  hgmapadd  39915  hlhilipval  39974  hlhilhillem  39985  mhphf  40292  mhphf2  40293  prjspval  40449  prjspner1  40470  mnringvald  41833  ioorrnopnlem  43852  hoidmvval0b  44135  hoidmvlelem2  44141  hoidmvlelem3  44142  hoidmvle  44145  ovnhoi  44148  hoiqssbl  44170  hspmbllem2  44172  vonioo  44227  vonicc  44230  ismgmd  45341  ismgmhm  45348  issubmgm  45354  resmgmhm  45363  resmgmhm2  45364  resmgmhm2b  45365  idfusubc  45435  rnghmval  45460  lidlmsgrp  45495  lidlrng  45496  zlidlring  45497  uzlidlring  45498  rnghmresel  45533  rngchom  45536  rngcco  45540  rnghmsubcsetclem1  45544  rhmresel  45579  ringchom  45582  ringcco  45586  rhmsubcsetclem1  45590  rhmsubcrngclem1  45596  irinitoringc  45638  ovmpordxf  45685  lincop  45760  lincval  45761  lincsum  45781  lincscm  45782  lmod1lem2  45840  lmod1lem3  45841  lmod1lem4  45842  ldepsnlinc  45860  lines  46088  line  46089  rrxlines  46090  rrxline  46091  spheres  46103  fvconstr  46194  fvconstrn0  46195  fvconstr2  46196  catprs  46303  thincmod  46323  isthincd2lem2  46328  isthincd  46329  mndtcco2  46384  mndtccatid  46385  grptcmon  46388  grptcepi  46389