Theorem oveqd 7369

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

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

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 4859  df-br 5094  df-iota 6443  df-fv 6495  df-ov 7355

This theorem is referenced by:  oveq123d  7373  oveqdr  7380  csbov  7397  csbov12g  7398  ovmpodxf  7502  oprssov  7521  2mpo0  7601  ofeqd  7618  mptmpoopabbrd  8018  mptmpoopabbrdOLD  8019  mptmpoopabovd  8020  el2mpocsbcl  8021  fnmpoovd  8023  frecseq123  8218  ruclem1  16146  vdwapval  16891  vdwapid1  16893  vdwmc2  16897  vdwpc  16898  vdwlem5  16903  vdwlem8  16906  vdwlem13  16911  prdsval  17365  prdsdsval2  17394  pwsplusgval  17400  pwsmulrval  17401  pwsvscafval  17404  imasval  17421  iscat  17584  iscatd  17585  catidex  17586  catideu  17587  cidfval  17588  cidval  17589  catidd  17592  iscatd2  17593  catlid  17595  catrid  17596  homffval  17602  homfeqd  17607  homfeqval  17609  comfffval  17610  comffval  17611  comfeq  17618  comfeqd  17619  comfeqval  17620  catpropd  17621  oppcval  17625  oppcco  17629  monfval  17645  ismon  17646  oppcmon  17651  oppcepi  17652  sectffval  17663  sectfval  17664  invffval  17671  isoval  17678  dfiso2  17685  isofn  17688  invisoinvl  17703  invcoisoid  17705  isocoinvid  17706  issubc  17748  issubc3  17762  isfunc  17777  cofuval  17795  cofuval2  17800  funcres  17809  funcres2b  17810  funcres2  17811  idfusubc  17813  funcres2c  17816  isfull  17825  isfth  17829  fullres2c  17854  natfval  17862  isnat  17863  fucval  17874  fucco  17878  fucpropd  17893  initoval  17906  termoval  17907  homarcl  17941  coafval  17977  resssetc  18005  resscatc  18022  catciso  18024  xpcval  18089  1stfval  18103  2ndfval  18106  prfval  18111  prfcl  18115  evlfval  18129  curfval  18135  curf1cl  18140  curfcl  18144  uncf1  18148  uncf2  18149  diag12  18156  diag2  18157  curf2ndf  18159  hofval  18164  hof1  18166  hof2fval  18167  hofcl  18171  yon12  18177  yon2  18178  hofpropd  18179  joinval  18287  meetval  18301  isdlat  18434  plusffval  18560  ismgmd  18566  issstrmgm  18567  grpidval  18575  grpidd  18585  gsumvalx  18590  gsumpropd  18592  gsumress  18596  ismgmhm  18610  issubmgm  18616  resmgmhm  18625  resmgmhm2  18626  resmgmhm2b  18627  issgrpd  18644  ismndd  18670  issubmnd  18675  submnd0  18677  ismhm  18699  issubm  18717  resmhm  18734  resmhm2  18735  resmhm2b  18736  mhmimalem  18738  isgrp  18858  isgrpd2e  18874  grpidd2  18896  grpinvfval  18897  grpinvfvalALT  18898  imasgrp2  18974  imasgrp  18975  subg0  19051  subginv  19052  subgcl  19055  issubgrpd2  19061  isnsg  19073  isghm  19133  isghmOLD  19134  resghm  19150  isga  19209  subgga  19218  gasubg  19220  cntzfval  19238  resscntz  19251  odfval  19450  odfvalALT  19451  gexval  19496  lsmfval  19556  lsmvalx  19557  oppglsm  19560  subglsm  19591  pj1fval  19612  efgtval  19641  iscmn  19707  iscmnd  19712  submcmn2  19757  imasabl  19794  iscyg  19797  cycsubmcmn  19807  isomnd  20041  submomnd  20050  prdsmgp  20075  rngpropd  20098  ringurd  20109  issrg  20112  isring  20161  ringidss  20201  mulgass3  20277  dvdsrval  20285  rdivmuldivd  20337  isirred  20343  rnghmval  20364  islring  20461  lringuplu  20465  subrngmcl  20478  subrg1  20503  subrgdvds  20507  subrguss  20508  subrginv  20509  subrgdv  20510  subrgunit  20511  subrgugrp  20512  rnghmresel  20541  rngchom  20544  rngcco  20548  rnghmsubcsetclem1  20552  rhmresel  20570  ringchom  20573  ringcco  20577  rhmsubcsetclem1  20581  rhmsubcrngclem1  20587  rrgval  20618  isdrngd  20686  isdrngrd  20687  isdrngdOLD  20688  isdrngrdOLD  20689  abvfval  20731  isabvd  20733  issrngd  20776  isorng  20782  suborng  20797  islmod  20803  islmodd  20805  scaffval  20819  lmodpropd  20864  lssset  20872  islssd  20874  prdslmodd  20908  islmhm  20967  reslmhm  20992  reslmhm2  20993  reslmhm2b  20994  islbs  21016  rlmvneg  21146  rnglidlmmgm  21188  rnglidlmsgrp  21189  rnglidlrng  21190  rngqiprngghmlem3  21232  rngqiprngimfolem  21233  rngqiprnglinlem1  21234  rngqiprngimf1  21243  rngqiprnglin  21245  rng2idl1cntr  21248  rngqiprngfulem5  21258  irinitoringc  21422  isphl  21571  ipffval  21591  isphld  21597  phssipval  21600  phssip  21601  phlssphl  21602  ocvfval  21609  isobs  21663  frlmplusgval  21707  frlmsubgval  21708  frlmvscafval  21709  frlmip  21721  frlmipval  21722  frlmup1  21741  lsslindf  21773  isassa  21799  isassad  21808  sraassab  21811  assamulgscmlem2  21843  psrval  21858  resspsradd  21918  resspsrmul  21919  resspsrvsca  21920  mplmon2mul  22010  ply1coe  22219  ply1chr  22227  lply1binomsc  22232  evl1expd  22266  evl1scvarpw  22284  asclply1subcl  22295  mamufval  22313  matplusg2  22348  matvsca2  22349  matplusgcell  22354  matsubgcell  22355  matinvgcell  22356  matvscacell  22357  matmulcell  22366  mpomatmul  22367  mat1  22368  mattposm  22380  mat1dimmul  22397  dmatmul  22418  dmatcrng  22423  scmataddcl  22437  scmatsubcl  22438  scmatcrng  22442  smatvscl  22445  scmatghm  22454  scmatmhm  22455  mvmulfval  22463  ma1repveval  22492  mdetrlin  22523  mdetrsca  22524  mdetmul  22544  madurid  22565  minmar1cl  22572  smadiadetglem1  22592  smadiadetr  22596  matinv  22598  slesolinv  22601  slesolinvbi  22602  cramerimplem3  22606  cpmatacl  22637  mat2pmatghm  22651  decpmatmullem  22692  decpmatmul  22693  pmatcollpw1lem1  22695  pmatcollpw2lem  22698  pmatcollpwlem  22701  pmatcollpw3lem  22704  mply1topmatval  22725  mp2pm2mplem1  22727  mp2pm2mplem4  22730  mp2pm2mplem5  22731  mp2pm2mp  22732  chpmat1d  22757  chpscmatgsummon  22766  chfacfpmmulgsum2  22786  xkocnv  23735  submtmd  24025  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  28222  istrkgc  28438  istrkgb  28439  istrkgcb  28440  istrkge  28441  istrkgl  28442  istrkgld  28443  iscgrg  28496  isismt  28518  tglngval  28535  legval  28568  ishlg  28586  mirval  28639  israg  28681  ishpg  28743  lmif  28769  islmib  28771  isinag  28822  ttgval  28859  wksonproplem  29688  wspthsnon  29837  iswwlksnon  29838  iswspthsnon  29841  isconngr  30176  isconngr1  30177  grpodivval  30522  dipfval  30689  ipval  30690  sspgval  30716  sspsval  30718  lnoval  30739  ajfval  30796  dipdir  30829  dipass  30832  htth  30905  ressmulgnn0d  33032  inftmrel  33156  isinftm  33157  isslmd  33178  elrgspnlem1  33216  erlval  33232  rlocval  33233  rlocaddval  33242  rlocmulval  33243  subrdom  33258  resv1r  33311  lsmidllsp  33372  idlinsubrg  33403  prmidlval  33409  idlsrgval  33475  idlsrg0g  33478  rprmval  33488  ressply1evls1  33535  drgextlsp  33613  fedgmullem1  33649  fedgmullem2  33650  fedgmul  33651  extdg1id  33686  fldextrspunlsplem  33693  fldextrspunlsp  33694  extdgfialglem1  33712  extdgfialglem2  33713  algextdeglem8  33744  smatlem  33817  submatminr1  33830  metidval  33910  pstmval  33915  pstmfval  33916  zlm0  33980  zlm1  33981  sitmval  34369  breprexp  34653  istrkg2d  34686  afsval  34691  mclsrcl  35612  mppsval  35623  bj-endval  37366  matunitlindflem2  37663  istotbnd  37815  isbnd  37826  rrnequiv  37881  isrngo  37943  rngohomval  38010  idlval  38059  pridlval  38079  lflset  39164  islfld  39167  ldualvadd  39234  ldualsmul  39240  ldualvs  39242  isopos  39285  cmtfvalN  39315  iscvlat  39428  ishlat1  39457  lineset  39843  psubspset  39849  paddfval  39902  paddval  39903  ltrnfset  40222  trnfsetN  40260  trlfset  40265  tgrpov  40853  erngplus  40908  erngmul  40911  erngplus-rN  40916  erngmul-rN  40919  erngdvlem3  41095  erngdvlem4  41096  erng0g  41099  erngdvlem3-rN  41103  erngdvlem4-rN  41104  dvaplusg  41114  dvamulr  41117  dvavadd  41120  dvavsca  41122  dvalveclem  41130  dvhmulr  41191  dvhfvadd  41196  dvhvadd  41197  dvhopvadd2  41199  dvhvaddcl  41200  dvhvaddcomN  41201  dvhvsca  41206  dvhlveclem  41213  dvh0g  41216  djavalN  41240  diblsmopel  41276  dicvaddcl  41295  cdlemn6  41307  dihffval  41335  dihopelvalcpre  41353  djhval  41503  lcdvaddval  41703  lcdsmul  41707  lcdvsval  41709  lcdlkreq2N  41728  hvmapffval  41863  hvmapfval  41864  hdmap1fval  41901  hgmapffval  41990  hgmapfval  41991  hgmapadd  41999  hlhilipval  42054  hlhilhillem  42065  isprimroot  42192  aks6d1c1p4  42210  idomnnzpownz  42231  aks6d1c5lem1  42235  aks6d1c5lem3  42236  aks6d1c5lem2  42237  aks5lem3a  42288  unitscyglem5  42298  rhmpsr1  42652  selvvvval  42684  mhphf2  42697  prjspval  42702  prjspner1  42725  sn-isghm  42772  mnringvald  44311  ioorrnopnlem  46407  hoidmvval0b  46693  hoidmvlelem2  46699  hoidmvlelem3  46700  hoidmvle  46703  ovnhoi  46706  hoiqssbl  46728  hspmbllem2  46730  vonioo  46785  vonicc  46788  zlidlring  48339  uzlidlring  48340  ovmpordxf  48444  lincop  48514  lincval  48515  lincsum  48535  lincscm  48536  lmod1lem2  48594  lmod1lem3  48595  lmod1lem4  48596  ldepsnlinc  48614  lines  48837  line  48838  rrxlines  48839  rrxline  48840  spheres  48852  fvconstr  48967  fvconstrn0  48968  fvconstr2  48969  catprs  49117  sectrcl2  49129  invrcl2  49131  invfn  49136  isorcl2  49140  sectpropdlem  49142  invpropdlem  49144  isopropdlem  49146  cicpropdlem  49155  iinfconstbas  49172  nelsubclem  49173  nelsubc3lem  49176  ssccatid  49178  resccatlem  49179  cofu2a  49201  cofid2a  49219  cofid2  49221  cofidf2a  49223  cofidf2  49226  oppf2  49246  upfval  49282  upfval2  49283  upfval3  49284  upeu3  49301  upeu4  49302  oppcup3  49315  natoppfb  49337  swapfval  49368  swapf2a  49377  1stfpropd  49396  2ndfpropd  49397  cofuswapf2  49401  tposcurf12  49404  tposcurf2  49406  tposcurf2cl  49408  fucofvalg  49424  fuco11b  49443  fuco23a  49458  precofval3  49477  prcofpropd  49485  catcrcl2  49502  opf12  49510  fucoppcco  49515  thincmod  49536  isthincd2lem2  49541  isthincd  49542  dfinito4  49607  mndtcco2  49692  mndtccatid  49693  oppgoppchom  49696  oppgoppcco  49697  grptcmon  49699  grptcepi  49700  2arwcatlem2  49702  2arwcatlem3  49703  2arwcatlem4  49704  2arwcat  49706  lanrcl  49727  ranrcl  49728  rellan  49729  relran  49730  concom  49769  coccom  49770