Theorem oveqd 7272

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  oveq123d  7276  oveqdr  7283  csbov  7298  csbov12g  7299  ovmpodxf  7401  oprssov  7419  2mpo0  7496  ofeqd  7513  mptmpoopabbrd  7894  mptmpoopabovd  7895  el2mpocsbcl  7896  fnmpoovd  7898  frecseq123  8069  ruclem1  15868  vdwapval  16602  vdwapid1  16604  vdwmc2  16608  vdwpc  16609  vdwlem5  16614  vdwlem8  16617  vdwlem13  16622  prdsval  17083  prdsdsval2  17112  pwsplusgval  17118  pwsmulrval  17119  pwsvscafval  17122  imasval  17139  iscat  17298  iscatd  17299  catidex  17300  catideu  17301  cidfval  17302  cidval  17303  catidd  17306  iscatd2  17307  catlid  17309  catrid  17310  homffval  17316  homfeqd  17321  homfeqval  17323  comfffval  17324  comffval  17325  comfeq  17332  comfeqd  17333  comfeqval  17334  catpropd  17335  oppcval  17339  oppcco  17344  monfval  17361  ismon  17362  oppcmon  17367  oppcepi  17368  sectffval  17379  sectfval  17380  invffval  17387  isoval  17394  dfiso2  17401  isofn  17404  invisoinvl  17419  invcoisoid  17421  isocoinvid  17422  issubc  17466  issubc3  17480  isfunc  17495  cofuval  17513  cofuval2  17518  funcres  17527  funcres2b  17528  funcres2  17529  funcres2c  17533  isfull  17542  isfth  17546  fullres2c  17571  natfval  17578  isnat  17579  fucval  17591  fucco  17596  fucpropd  17611  initoval  17624  termoval  17625  homarcl  17659  coafval  17695  resssetc  17723  resscatc  17740  catciso  17742  xpcval  17810  1stfval  17824  2ndfval  17827  prfval  17832  prfcl  17836  evlfval  17851  curfval  17857  curf1cl  17862  curfcl  17866  uncf1  17870  uncf2  17871  diag12  17878  diag2  17879  curf2ndf  17881  hofval  17886  hof1  17888  hof2fval  17889  hofcl  17893  yon12  17899  yon2  17900  hofpropd  17901  joinval  18010  meetval  18024  isdlat  18155  plusffval  18247  issstrmgm  18252  grpidval  18260  grpidd  18270  gsumvalx  18275  gsumpropd  18277  gsumress  18281  ismndd  18322  issubmnd  18327  submnd0  18329  ismhm  18347  issubm  18357  resmhm  18374  resmhm2  18375  resmhm2b  18376  isgrp  18498  isgrpd2e  18513  grpidd2  18532  grpinvfval  18533  grpinvfvalALT  18534  imasgrp2  18605  imasgrp  18606  subg0  18676  subginv  18677  subgcl  18680  issubgrpd2  18686  isnsg  18698  isghm  18749  resghm  18765  isga  18812  subgga  18821  gasubg  18823  cntzfval  18841  resscntz  18853  odfval  19055  odfvalALT  19056  gexval  19098  lsmfval  19158  lsmvalx  19159  oppglsm  19162  subglsm  19194  pj1fval  19215  efgtval  19244  iscmn  19309  iscmnd  19314  submcmn2  19355  iscyg  19394  cycsubmcmn  19404  issrg  19658  isring  19702  ringidss  19731  prdsmgp  19764  mulgass3  19794  dvdsrval  19802  isirred  19856  isdrngd  19931  isdrngrd  19932  subrg1  19949  subrgmcl  19951  subrgdvds  19953  subrguss  19954  subrginv  19955  subrgdv  19956  subrgunit  19957  subrgugrp  19958  abvfval  19993  isabvd  19995  issrngd  20036  islmod  20042  islmodd  20044  scaffval  20056  lmodpropd  20101  lssset  20110  islssd  20112  prdslmodd  20146  islmhm  20204  reslmhm  20229  reslmhm2  20230  reslmhm2b  20231  islbs  20253  rlmvneg  20391  rrgval  20471  isphl  20745  ipffval  20765  isphld  20771  phssipval  20774  phssip  20775  phlssphl  20776  ocvfval  20783  isobs  20837  frlmplusgval  20881  frlmsubgval  20882  frlmvscafval  20883  frlmip  20895  frlmipval  20896  frlmup1  20915  lsslindf  20947  isassa  20973  isassad  20981  assamulgscmlem2  21014  psrval  21028  resspsradd  21095  resspsrmul  21096  resspsrvsca  21097  mplmon2mul  21187  ply1coe  21377  lply1binomsc  21388  evl1expd  21421  evl1scvarpw  21439  mamufval  21444  matplusg2  21484  matvsca2  21485  matplusgcell  21490  matsubgcell  21491  matinvgcell  21492  matvscacell  21493  matmulcell  21502  mpomatmul  21503  mat1  21504  mattposm  21516  mat1dimmul  21533  dmatmul  21554  dmatcrng  21559  scmataddcl  21573  scmatsubcl  21574  scmatcrng  21578  smatvscl  21581  scmatghm  21590  scmatmhm  21591  mvmulfval  21599  ma1repveval  21628  mdetrlin  21659  mdetrsca  21660  mdetmul  21680  madurid  21701  minmar1cl  21708  smadiadetglem1  21728  smadiadetr  21732  matinv  21734  slesolinv  21737  slesolinvbi  21738  cramerimplem3  21742  cpmatacl  21773  mat2pmatghm  21787  decpmatmullem  21828  decpmatmul  21829  pmatcollpw1lem1  21831  pmatcollpw2lem  21834  pmatcollpwlem  21837  pmatcollpw3lem  21840  mply1topmatval  21861  mp2pm2mplem1  21863  mp2pm2mplem4  21866  mp2pm2mplem5  21867  mp2pm2mp  21868  chpmat1d  21893  chpscmatgsummon  21902  chfacfpmmulgsum2  21922  xkocnv  22873  submtmd  23163  prdsdsf  23428  ressprdsds  23432  blfvalps  23444  prdsxmslem2  23591  tmsxpsval  23600  ngpds  23666  sgrimval  23694  subgngp  23697  tngngp  23724  tngngp3  23726  isnlm  23745  lssnlm  23771  isphtpy  24050  isphtpc  24063  pi1cpbl  24113  pi1addf  24116  pi1addval  24117  pi1grplem  24118  clmsub  24149  clmvsass  24158  clmvsdir  24160  isclmp  24166  cvsdiv  24201  iscph  24239  cphdir  24274  cphdi  24275  cph2di  24276  cph2subdi  24279  cphass  24280  tcphval  24287  ipcau2  24303  tcphcphlem1  24304  tcphcphlem2  24305  cphsscph  24320  caufval  24344  rrxip  24459  rrxvsca  24463  rrxplusgvscavalb  24464  rrxdsfival  24482  ehleudisval  24488  dvlip2  25064  q1pval  25223  r1pval  25226  dvntaylp  25435  efabl  25611  efsubm  25612  dchrmul  26301  istrkgc  26719  istrkgb  26720  istrkgcb  26721  istrkge  26722  istrkgl  26723  istrkgld  26724  iscgrg  26777  isismt  26799  tglngval  26816  legval  26849  ishlg  26867  mirval  26920  israg  26962  ishpg  27024  lmif  27050  islmib  27052  isinag  27103  ttgval  27140  wksonproplem  27974  wspthsnon  28118  iswwlksnon  28119  iswspthsnon  28122  isconngr  28454  isconngr1  28455  grpodivval  28798  dipfval  28965  ipval  28966  sspgval  28992  sspsval  28994  lnoval  29015  ajfval  29072  dipdir  29105  dipass  29108  htth  29181  isomnd  31229  submomnd  31238  inftmrel  31336  isinftm  31337  isslmd  31357  rngurd  31384  rdivmuldivd  31390  isorng  31400  suborng  31416  resv1r  31443  lsmidllsp  31490  idlinsubrg  31510  prmidlval  31514  idlsrgval  31550  idlsrg0g  31553  rprmval  31566  ply1chr  31571  drgextlsp  31583  fedgmullem1  31612  fedgmullem2  31613  fedgmul  31614  extdg1id  31640  smatlem  31649  submatminr1  31662  metidval  31742  pstmval  31747  pstmfval  31748  zlm0  31812  zlm1  31813  sitmval  32216  breprexp  32513  istrkg2d  32546  afsval  32551  mclsrcl  33423  mppsval  33434  bj-endval  35413  matunitlindflem2  35701  istotbnd  35854  isbnd  35865  rrnequiv  35920  isrngo  35982  rngohomval  36049  idlval  36098  pridlval  36118  lflset  37000  islfld  37003  ldualvadd  37070  ldualsmul  37076  ldualvs  37078  isopos  37121  cmtfvalN  37151  iscvlat  37264  ishlat1  37293  lineset  37679  psubspset  37685  paddfval  37738  paddval  37739  ltrnfset  38058  trnfsetN  38096  trlfset  38101  tgrpov  38689  erngplus  38744  erngmul  38747  erngplus-rN  38752  erngmul-rN  38755  erngdvlem3  38931  erngdvlem4  38932  erng0g  38935  erngdvlem3-rN  38939  erngdvlem4-rN  38940  dvaplusg  38950  dvamulr  38953  dvavadd  38956  dvavsca  38958  dvalveclem  38966  dvhmulr  39027  dvhfvadd  39032  dvhvadd  39033  dvhopvadd2  39035  dvhvaddcl  39036  dvhvaddcomN  39037  dvhvsca  39042  dvhlveclem  39049  dvh0g  39052  djavalN  39076  diblsmopel  39112  dicvaddcl  39131  cdlemn6  39143  dihffval  39171  dihopelvalcpre  39189  djhval  39339  lcdvaddval  39539  lcdsmul  39543  lcdvsval  39545  lcdlkreq2N  39564  hvmapffval  39699  hvmapfval  39700  hdmap1fval  39737  hgmapffval  39826  hgmapfval  39827  hgmapadd  39835  hlhilipval  39894  hlhilhillem  39905  mhphf  40208  mhphf2  40209  prjspval  40363  prjspner1  40384  mnringvald  41715  ioorrnopnlem  43735  hoidmvval0b  44018  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvle  44028  ovnhoi  44031  hoiqssbl  44053  hspmbllem2  44055  vonioo  44110  vonicc  44113  ismgmd  45218  ismgmhm  45225  issubmgm  45231  resmgmhm  45240  resmgmhm2  45241  resmgmhm2b  45242  idfusubc  45312  rnghmval  45337  lidlmsgrp  45372  lidlrng  45373  zlidlring  45374  uzlidlring  45375  rnghmresel  45410  rngchom  45413  rngcco  45417  rnghmsubcsetclem1  45421  rhmresel  45456  ringchom  45459  ringcco  45463  rhmsubcsetclem1  45467  rhmsubcrngclem1  45473  irinitoringc  45515  ovmpordxf  45562  lincop  45637  lincval  45638  lincsum  45658  lincscm  45659  lmod1lem2  45717  lmod1lem3  45718  lmod1lem4  45719  ldepsnlinc  45737  lines  45965  line  45966  rrxlines  45967  rrxline  45968  spheres  45980  fvconstr  46071  fvconstrn0  46072  fvconstr2  46073  catprs  46180  thincmod  46200  isthincd2lem2  46205  isthincd  46206  mndtcco2  46259  mndtccatid  46260  grptcmon  46263  grptcepi  46264