Theorem oveqd 7426

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  (class class class)co 7409

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-uni 4868  df-br 5104  df-iota 6484  df-fv 6536  df-ov 7412

This theorem is used by:  oveq123d  7430  oveqdr  7437  csbov  7454  csbov12g  7455  ovmpodxf  7559  oprssov  7579  2mpo0  7659  ofeqd  7679  mptmpoopabbrd  8078  mptmpoopabovd  8079  el2mpocsbcl  8080  fnmpoovd  8082  frecseq123  8279  ruclem1  16352  vdwapval  17098  vdwapid1  17100  vdwmc2  17104  vdwpc  17105  vdwlem5  17110  vdwlem8  17113  vdwlem13  17118  prdsval  17573  prdsdsval2  17602  pwsplusgval  17609  pwsmulrval  17610  pwsvscafval  17613  imasval  17630  iscat  17793  iscatd  17794  catidex  17795  catideu  17796  cidfval  17797  cidval  17798  catidd  17801  iscatd2  17802  catlid  17804  catrid  17805  homffval  17811  homfeqd  17816  homfeqval  17818  comfffval  17819  comffval  17820  comfeq  17827  comfeqd  17828  comfeqval  17829  catpropd  17830  oppcval  17834  oppcco  17838  monfval  17854  ismon  17855  oppcmon  17860  oppcepi  17861  sectffval  17872  sectfval  17873  invffval  17880  isoval  17887  dfiso2  17894  isofn  17897  invisoinvl  17912  invcoisoid  17914  isocoinvid  17915  issubc  17957  issubc3  17971  isfunc  17986  cofuval  18004  cofuval2  18009  funcres  18018  funcres2b  18019  funcres2  18020  idfusubc  18022  funcres2c  18025  isfull  18034  isfth  18038  fullres2c  18063  natfval  18071  isnat  18072  fucval  18083  fucco  18087  fucpropd  18102  initoval  18115  termoval  18116  homarcl  18150  coafval  18186  resssetc  18214  resscatc  18231  catciso  18233  xpcval  18298  1stfval  18312  2ndfval  18315  prfval  18320  prfcl  18324  evlfval  18338  curfval  18344  curf1cl  18349  curfcl  18353  uncf1  18357  uncf2  18358  diag12  18365  diag2  18366  curf2ndf  18368  hofval  18373  hof1  18375  hof2fval  18376  hofcl  18380  yon12  18386  yon2  18387  hofpropd  18388  joinval  18496  meetval  18510  isdlat  18643  plusffval  18769  ismgmd  18777  issstrmgm  18778  grpidval  18787  grpidd  18799  idressid  18809  gsumvalx  18812  gsumpropd  18814  gsumress  18818  ismgmhm  18832  issubmgm  18838  resmgmhm  18847  resmgmhm2  18848  resmgmhm2b  18849  issgrpd  18866  ismndd  18893  issubmnd  18900  submnd0OLD  18904  ismhm  18927  issubm  18945  resmhm  18963  resmhm2  18964  resmhm2b  18965  mhmimalem  18967  isgrp  19097  isgrpd2e  19113  grpidd2  19135  grpinvfval  19136  grpinvfvalALT  19137  imasgrp2  19212  imasgrp  19213  subg0  19289  subginv  19290  subgcl  19293  issubgrpd2  19300  isnsg  19312  isghm  19377  resghm  19393  isga  19452  subgga  19461  gasubg  19463  cntzfval  19481  resscntz  19494  odfval  19693  odfvalALT  19694  gexval  19739  lsmfval  19799  lsmvalx  19800  oppglsm  19803  subglsm  19834  pj1fval  19855  efgtval  19884  iscmn  19950  iscmnd  19955  submcmn2  20000  imasabl  20037  iscyg  20040  cycsubmcmn  20050  isomnd  20284  submomnd  20293  prdsmgp  20318  rngpropd  20343  ringurd  20358  issrg  20361  isring  20410  ringidss  20453  mulgass3  20530  dvdsrval  20538  rdivmuldivd  20590  isirred  20596  rnghmval  20617  rhmval0  20652  islring  20739  lringuplu  20743  subrngmcl  20756  subrg1  20781  subrgdvds  20785  subrguss  20786  subrginv  20787  subrgdv  20788  subrgunit  20789  subrgugrp  20790  rnghmresel  20819  rngchom  20822  rngcco  20826  rnghmsubcsetclem1  20830  rhmresel  20848  ringchom  20851  ringcco  20855  rhmsubcsetclem1  20859  rhmsubcrngclem1  20865  rrgval  20896  isdrngd  20969  isdrngrd  20970  isdrngdOLD  20971  isdrngrdOLD  20972  abvfval  21014  isabvd  21016  issrngd  21059  isorng  21065  suborng  21080  islmod  21086  islmodd  21088  scaffval  21102  lmodpropd  21147  lssset  21155  islssd  21157  prdslmodd  21191  islmhm  21249  reslmhm  21274  reslmhm2  21275  reslmhm2b  21276  islbs  21298  rlmvneg  21428  rnglidlmmgm  21480  rnglidlmsgrp  21481  rnglidlrng  21482  lsmidllsp  21484  rngqiprngghmlem3  21532  rngqiprngimfolem  21533  rngqiprnglinlem1  21534  rngqiprngimf1  21543  rngqiprnglin  21545  rng2idl1cntr  21548  rngqiprngfulem5  21558  prmidlval  21565  irinitoringc  21732  isphl  21881  ipffval  21901  isphld  21907  phssipval  21910  phssip  21911  phlssphl  21912  ocvfval  21919  isobs  21973  frlmplusgval  22017  frlmsubgval  22018  frlmvscafval  22019  frlmip  22031  frlmipval  22032  frlmup1  22051  lsslindf  22083  isassa  22111  isassad  22120  sraassab  22123  assamulgscmlem2  22155  psrval  22170  resspsradd  22229  resspsrmul  22230  resspsrvsca  22231  mplmon2mul  22325  selvvvval  22398  ply1coe  22563  ply1chr  22571  lply1binomsc  22576  evl1expd  22610  evl1scvarpw  22628  asclply1subcl  22639  mamufval  22654  matplusg2  22689  matvsca2  22690  matplusgcell  22695  matsubgcell  22696  matinvgcell  22697  matvscacell  22698  matmulcell  22707  mpomatmul  22708  mat1  22709  mattposm  22721  mat1dimmul  22738  dmatmul  22759  dmatcrng  22764  scmataddcl  22778  scmatsubcl  22779  scmatcrng  22783  smatvscl  22786  scmatghm  22795  scmatmhm  22796  mvmulfval  22804  ma1repveval  22833  mdetrlin  22864  mdetrsca  22865  mdetmul  22885  madurid  22906  minmar1cl  22913  smadiadetglem1  22933  smadiadetr  22937  matinv  22939  matunitlindflem2  22942  slesolinv  22945  slesolinvbi  22946  cramerimplem3  22950  cpmatacl  22981  mat2pmatghm  22995  decpmatmullem  23036  decpmatmul  23037  pmatcollpw1lem1  23039  pmatcollpw2lem  23042  pmatcollpwlem  23045  pmatcollpw3lem  23048  mply1topmatval  23069  mp2pm2mplem1  23071  mp2pm2mplem4  23074  mp2pm2mplem5  23075  mp2pm2mp  23076  chpmat1d  23101  chpscmatgsummon  23110  chfacfpmmulgsum2  23130  xkocnv  24080  submtmd  24370  prdsdsf  24633  ressprdsds  24637  blfvalps  24649  prdsxmslem2  24795  tmsxpsval  24804  ngpds  24870  sgrimval  24898  subgngp  24901  tngngp  24920  tngngp3  24922  isnlm  24941  lssnlm  24967  isphtpy  25249  isphtpc  25262  pi1cpbl  25312  pi1addf  25315  pi1addval  25316  pi1grplem  25317  clmsub  25348  clmvsass  25357  clmvsdir  25359  isclmp  25365  cvsdiv  25400  iscph  25438  cphdir  25473  cphdi  25474  cph2di  25475  cph2subdi  25478  cphass  25479  tcphval  25486  ipcau2  25502  tcphcphlem1  25503  tcphcphlem2  25504  cphsscph  25519  caufval  25543  rrxip  25658  rrxvsca  25662  rrxplusgvscavalb  25663  rrxdsfival  25681  ehleudisval  25687  dvlip2  26262  q1pval  26420  r1pval  26423  dvntaylp  26647  efabl  26827  efsubm  26828  dchrmul  27524  seqseq123d  28591  istrkgc  28835  istrkgb  28836  istrkgcb  28837  istrkge  28838  istrkgl  28839  istrkgld  28840  iscgrg  28894  isismt  28916  tglngval  28933  legval  28966  ishlg2  28984  ishlg  28987  mirval  29046  israg  29091  ishpg  29156  tgplnfn  29172  plngval  29174  isplng  29175  lmif  29209  islmib  29211  isinag  29276  angmgmval  29313  ttgval  29371  wksonproplem  30206  wspthsnon  30360  iswwlksnon  30361  iswspthsnon  30364  isconngr  30709  isconngr1  30710  grpodivval  31056  dipfval  31223  ipval  31224  sspgval  31250  sspsval  31252  lnoval  31273  ajfval  31330  dipdir  31363  dipass  31366  htth  31439  ressmulgnn0d  33524  inftmrel  33660  isinftm  33661  isslmd  33682  elrgspnlem1  33722  erlval  33738  rlocval  33739  rlocaddval  33749  rlocmulval  33750  subrdom  33765  resv1r  33819  idlinsubrg  33900  idlsrgval  33954  idlsrg0g  33957  rprmval  33967  ressply1evls1  34016  vietalem  34130  drgextlsp  34145  fedgmullem1  34180  fedgmullem2  34181  fedgmul  34182  extdg1id  34217  fldextrspunlsplem  34224  fldextrspunlsp  34225  extdgfialglem1  34243  extdgfialglem2  34244  algextdeglem8  34275  smatlem  34348  submatminr1  34361  metidval  34441  pstmval  34446  pstmfval  34447  zlm0  34511  zlm1  34512  sitmval  34901  breprexp  35182  istrkg2d  35215  afsval  35223  mclsrcl  36241  mppsval  36252  bj-endval  38150  istotbnd  38617  isbnd  38628  rrnequiv  38683  isrngo  38745  rngohomval  38812  idlval  38861  pridlval  38881  lflset  40030  islfld  40033  ldualvadd  40100  ldualsmul  40106  ldualvs  40108  isopos  40151  cmtfvalN  40181  iscvlat  40294  ishlat1  40323  lineset  40709  psubspset  40715  paddfval  40768  paddval  40769  ltrnfset  41088  trnfsetN  41126  trlfset  41131  tgrpov  41719  erngplus  41774  erngmul  41777  erngplus-rN  41782  erngmul-rN  41785  erngdvlem3  41961  erngdvlem4  41962  erng0g  41965  erngdvlem3-rN  41969  erngdvlem4-rN  41970  dvaplusg  41980  dvamulr  41983  dvavadd  41986  dvavsca  41988  dvalveclem  41996  dvhmulr  42057  dvhfvadd  42062  dvhvadd  42063  dvhopvadd2  42065  dvhvaddcl  42066  dvhvaddcomN  42067  dvhvsca  42072  dvhlveclem  42079  dvh0g  42082  djavalN  42106  diblsmopel  42142  dicvaddcl  42161  cdlemn6  42173  dihffval  42201  dihopelvalcpre  42219  djhval  42369  lcdvaddval  42569  lcdsmul  42573  lcdvsval  42575  lcdlkreq2N  42594  hvmapffval  42729  hvmapfval  42730  hdmap1fval  42767  hgmapffval  42856  hgmapfval  42857  hgmapadd  42865  hlhilipval  42920  hlhilhillem  42931  isprimroot  43057  aks6d1c1p4  43075  idomnnzpownz  43096  aks6d1c5lem1  43100  aks6d1c5lem3  43101  aks6d1c5lem2  43102  aks5lem3a  43153  unitscyglem5  43163  rhmpsr1  43528  mhphf2  43542  prjspval  43547  prjspner1  43570  sn-isghm  43617  mnringvald  45149  ioorrnopnlem  47230  hoidmvval0b  47516  hoidmvlelem2  47522  hoidmvlelem3  47523  hoidmvle  47526  ovnhoi  47529  hoiqssbl  47551  hspmbllem2  47553  vonioo  47608  vonicc  47611  zlidlring  49247  uzlidlring  49248  ovmpordxf  49367  lincop  49436  lincval  49437  lincsum  49457  lincscm  49458  lmod1lem2  49516  lmod1lem3  49517  lmod1lem4  49518  ldepsnlinc  49536  lines  49759  line  49760  rrxlines  49761  rrxline  49762  spheres  49774  ovconstbrd  49888  ovconstbrn0d  49889  elovconstbrd  49890  catprs  50035  sectrcl2  50047  invrcl2  50049  invfn  50054  isorcl2  50058  sectpropdlem  50060  invpropdlem  50062  isopropdlem  50064  cicpropdlem  50073  iinfconstbas  50090  nelsubclem  50091  nelsubc3lem  50094  ssccatid  50096  resccatlem  50097  cofu2a  50119  cofid2a  50137  cofid2  50139  cofidf2a  50141  cofidf2  50144  oppf2  50164  upfval  50200  upfval2  50201  upfval3  50202  upeu3  50219  upeu4  50220  oppcup3  50233  natoppfb  50255  swapfval  50286  swapf2a  50295  1stfpropd  50314  2ndfpropd  50315  cofuswapf2  50319  tposcurf12  50322  tposcurf2  50324  tposcurf2cl  50326  fucofvalg  50342  fuco11b  50361  fuco23a  50376  precofval3  50395  prcofpropd  50403  catcrcl2  50420  opf12  50428  fucoppcco  50433  thincmod  50454  isthincd2lem2  50459  isthincd  50460  dfinito4  50525  mndtcco2  50610  mndtccatid  50611  oppgoppchom  50614  oppgoppcco  50615  grptcmon  50617  grptcepi  50618  2arwcatlem2  50620  2arwcatlem3  50621  2arwcatlem4  50622  2arwcat  50624  lanrcl  50645  ranrcl  50646  rellan  50647  relran  50648  concom  50687  coccom  50688