Theorem oveqd 7377

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

Syntax hints:   → wi 4   = wceq 1542  (class class class)co 7360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3443  df-ss 3919  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-ov 7363

This theorem is referenced by:  oveq123d  7381  oveqdr  7388  csbov  7405  csbov12g  7406  ovmpodxf  7510  oprssov  7529  2mpo0  7609  ofeqd  7626  mptmpoopabbrd  8026  mptmpoopabbrdOLD  8027  mptmpoopabovd  8028  el2mpocsbcl  8029  fnmpoovd  8031  frecseq123  8226  ruclem1  16160  vdwapval  16905  vdwapid1  16907  vdwmc2  16911  vdwpc  16912  vdwlem5  16917  vdwlem8  16920  vdwlem13  16925  prdsval  17379  prdsdsval2  17408  pwsplusgval  17415  pwsmulrval  17416  pwsvscafval  17419  imasval  17436  iscat  17599  iscatd  17600  catidex  17601  catideu  17602  cidfval  17603  cidval  17604  catidd  17607  iscatd2  17608  catlid  17610  catrid  17611  homffval  17617  homfeqd  17622  homfeqval  17624  comfffval  17625  comffval  17626  comfeq  17633  comfeqd  17634  comfeqval  17635  catpropd  17636  oppcval  17640  oppcco  17644  monfval  17660  ismon  17661  oppcmon  17666  oppcepi  17667  sectffval  17678  sectfval  17679  invffval  17686  isoval  17693  dfiso2  17700  isofn  17703  invisoinvl  17718  invcoisoid  17720  isocoinvid  17721  issubc  17763  issubc3  17777  isfunc  17792  cofuval  17810  cofuval2  17815  funcres  17824  funcres2b  17825  funcres2  17826  idfusubc  17828  funcres2c  17831  isfull  17840  isfth  17844  fullres2c  17869  natfval  17877  isnat  17878  fucval  17889  fucco  17893  fucpropd  17908  initoval  17921  termoval  17922  homarcl  17956  coafval  17992  resssetc  18020  resscatc  18037  catciso  18039  xpcval  18104  1stfval  18118  2ndfval  18121  prfval  18126  prfcl  18130  evlfval  18144  curfval  18150  curf1cl  18155  curfcl  18159  uncf1  18163  uncf2  18164  diag12  18171  diag2  18172  curf2ndf  18174  hofval  18179  hof1  18181  hof2fval  18182  hofcl  18186  yon12  18192  yon2  18193  hofpropd  18194  joinval  18302  meetval  18316  isdlat  18449  plusffval  18575  ismgmd  18581  issstrmgm  18582  grpidval  18590  grpidd  18600  gsumvalx  18605  gsumpropd  18607  gsumress  18611  ismgmhm  18625  issubmgm  18631  resmgmhm  18640  resmgmhm2  18641  resmgmhm2b  18642  issgrpd  18659  ismndd  18685  issubmnd  18690  submnd0  18692  ismhm  18714  issubm  18732  resmhm  18749  resmhm2  18750  resmhm2b  18751  mhmimalem  18753  isgrp  18873  isgrpd2e  18889  grpidd2  18911  grpinvfval  18912  grpinvfvalALT  18913  imasgrp2  18989  imasgrp  18990  subg0  19066  subginv  19067  subgcl  19070  issubgrpd2  19076  isnsg  19088  isghm  19148  isghmOLD  19149  resghm  19165  isga  19224  subgga  19233  gasubg  19235  cntzfval  19253  resscntz  19266  odfval  19465  odfvalALT  19466  gexval  19511  lsmfval  19571  lsmvalx  19572  oppglsm  19575  subglsm  19606  pj1fval  19627  efgtval  19656  iscmn  19722  iscmnd  19727  submcmn2  19772  imasabl  19809  iscyg  19812  cycsubmcmn  19822  isomnd  20056  submomnd  20065  prdsmgp  20090  rngpropd  20113  ringurd  20124  issrg  20127  isring  20176  ringidss  20216  mulgass3  20293  dvdsrval  20301  rdivmuldivd  20353  isirred  20359  rnghmval  20380  islring  20477  lringuplu  20481  subrngmcl  20494  subrg1  20519  subrgdvds  20523  subrguss  20524  subrginv  20525  subrgdv  20526  subrgunit  20527  subrgugrp  20528  rnghmresel  20557  rngchom  20560  rngcco  20564  rnghmsubcsetclem1  20568  rhmresel  20586  ringchom  20589  ringcco  20593  rhmsubcsetclem1  20597  rhmsubcrngclem1  20603  rrgval  20634  isdrngd  20702  isdrngrd  20703  isdrngdOLD  20704  isdrngrdOLD  20705  abvfval  20747  isabvd  20749  issrngd  20792  isorng  20798  suborng  20813  islmod  20819  islmodd  20821  scaffval  20835  lmodpropd  20880  lssset  20888  islssd  20890  prdslmodd  20924  islmhm  20983  reslmhm  21008  reslmhm2  21009  reslmhm2b  21010  islbs  21032  rlmvneg  21162  rnglidlmmgm  21204  rnglidlmsgrp  21205  rnglidlrng  21206  rngqiprngghmlem3  21248  rngqiprngimfolem  21249  rngqiprnglinlem1  21250  rngqiprngimf1  21259  rngqiprnglin  21261  rng2idl1cntr  21264  rngqiprngfulem5  21274  irinitoringc  21438  isphl  21587  ipffval  21607  isphld  21613  phssipval  21616  phssip  21617  phlssphl  21618  ocvfval  21625  isobs  21679  frlmplusgval  21723  frlmsubgval  21724  frlmvscafval  21725  frlmip  21737  frlmipval  21738  frlmup1  21757  lsslindf  21789  isassa  21815  isassad  21824  sraassab  21827  assamulgscmlem2  21860  psrval  21875  resspsradd  21934  resspsrmul  21935  resspsrvsca  21936  mplmon2mul  22028  ply1coe  22246  ply1chr  22254  lply1binomsc  22259  evl1expd  22293  evl1scvarpw  22311  asclply1subcl  22322  mamufval  22340  matplusg2  22375  matvsca2  22376  matplusgcell  22381  matsubgcell  22382  matinvgcell  22383  matvscacell  22384  matmulcell  22393  mpomatmul  22394  mat1  22395  mattposm  22407  mat1dimmul  22424  dmatmul  22445  dmatcrng  22450  scmataddcl  22464  scmatsubcl  22465  scmatcrng  22469  smatvscl  22472  scmatghm  22481  scmatmhm  22482  mvmulfval  22490  ma1repveval  22519  mdetrlin  22550  mdetrsca  22551  mdetmul  22571  madurid  22592  minmar1cl  22599  smadiadetglem1  22619  smadiadetr  22623  matinv  22625  slesolinv  22628  slesolinvbi  22629  cramerimplem3  22633  cpmatacl  22664  mat2pmatghm  22678  decpmatmullem  22719  decpmatmul  22720  pmatcollpw1lem1  22722  pmatcollpw2lem  22725  pmatcollpwlem  22728  pmatcollpw3lem  22731  mply1topmatval  22752  mp2pm2mplem1  22754  mp2pm2mplem4  22757  mp2pm2mplem5  22758  mp2pm2mp  22759  chpmat1d  22784  chpscmatgsummon  22793  chfacfpmmulgsum2  22813  xkocnv  23762  submtmd  24052  prdsdsf  24315  ressprdsds  24319  blfvalps  24331  prdsxmslem2  24477  tmsxpsval  24486  ngpds  24552  sgrimval  24580  subgngp  24583  tngngp  24602  tngngp3  24604  isnlm  24623  lssnlm  24649  isphtpy  24940  isphtpc  24953  pi1cpbl  25004  pi1addf  25007  pi1addval  25008  pi1grplem  25009  clmsub  25040  clmvsass  25049  clmvsdir  25051  isclmp  25057  cvsdiv  25092  iscph  25130  cphdir  25165  cphdi  25166  cph2di  25167  cph2subdi  25170  cphass  25171  tcphval  25178  ipcau2  25194  tcphcphlem1  25195  tcphcphlem2  25196  cphsscph  25211  caufval  25235  rrxip  25350  rrxvsca  25354  rrxplusgvscavalb  25355  rrxdsfival  25373  ehleudisval  25379  dvlip2  25960  q1pval  26120  r1pval  26123  dvntaylp  26339  efabl  26519  efsubm  26520  dchrmul  27219  seqseq123d  28286  istrkgc  28530  istrkgb  28531  istrkgcb  28532  istrkge  28533  istrkgl  28534  istrkgld  28535  iscgrg  28588  isismt  28610  tglngval  28627  legval  28660  ishlg  28678  mirval  28731  israg  28773  ishpg  28835  lmif  28861  islmib  28863  isinag  28914  ttgval  28951  wksonproplem  29780  wspthsnon  29929  iswwlksnon  29930  iswspthsnon  29933  isconngr  30268  isconngr1  30269  grpodivval  30614  dipfval  30781  ipval  30782  sspgval  30808  sspsval  30810  lnoval  30831  ajfval  30888  dipdir  30921  dipass  30924  htth  30997  ressmulgnn0d  33129  inftmrel  33264  isinftm  33265  isslmd  33286  elrgspnlem1  33326  erlval  33342  rlocval  33343  rlocaddval  33352  rlocmulval  33353  subrdom  33369  resv1r  33422  lsmidllsp  33483  idlinsubrg  33514  prmidlval  33520  idlsrgval  33586  idlsrg0g  33589  rprmval  33599  ressply1evls1  33648  vietalem  33737  drgextlsp  33752  fedgmullem1  33788  fedgmullem2  33789  fedgmul  33790  extdg1id  33825  fldextrspunlsplem  33832  fldextrspunlsp  33833  extdgfialglem1  33851  extdgfialglem2  33852  algextdeglem8  33883  smatlem  33956  submatminr1  33969  metidval  34049  pstmval  34054  pstmfval  34055  zlm0  34119  zlm1  34120  sitmval  34508  breprexp  34792  istrkg2d  34825  afsval  34830  mclsrcl  35757  mppsval  35768  bj-endval  37522  matunitlindflem2  37820  istotbnd  37972  isbnd  37983  rrnequiv  38038  isrngo  38100  rngohomval  38167  idlval  38216  pridlval  38236  lflset  39387  islfld  39390  ldualvadd  39457  ldualsmul  39463  ldualvs  39465  isopos  39508  cmtfvalN  39538  iscvlat  39651  ishlat1  39680  lineset  40066  psubspset  40072  paddfval  40125  paddval  40126  ltrnfset  40445  trnfsetN  40483  trlfset  40488  tgrpov  41076  erngplus  41131  erngmul  41134  erngplus-rN  41139  erngmul-rN  41142  erngdvlem3  41318  erngdvlem4  41319  erng0g  41322  erngdvlem3-rN  41326  erngdvlem4-rN  41327  dvaplusg  41337  dvamulr  41340  dvavadd  41343  dvavsca  41345  dvalveclem  41353  dvhmulr  41414  dvhfvadd  41419  dvhvadd  41420  dvhopvadd2  41422  dvhvaddcl  41423  dvhvaddcomN  41424  dvhvsca  41429  dvhlveclem  41436  dvh0g  41439  djavalN  41463  diblsmopel  41499  dicvaddcl  41518  cdlemn6  41530  dihffval  41558  dihopelvalcpre  41576  djhval  41726  lcdvaddval  41926  lcdsmul  41930  lcdvsval  41932  lcdlkreq2N  41951  hvmapffval  42086  hvmapfval  42087  hdmap1fval  42124  hgmapffval  42213  hgmapfval  42214  hgmapadd  42222  hlhilipval  42277  hlhilhillem  42288  isprimroot  42415  aks6d1c1p4  42433  idomnnzpownz  42454  aks6d1c5lem1  42458  aks6d1c5lem3  42459  aks6d1c5lem2  42460  aks5lem3a  42511  unitscyglem5  42521  rhmpsr1  42873  selvvvval  42895  mhphf2  42908  prjspval  42913  prjspner1  42936  sn-isghm  42983  mnringvald  44521  ioorrnopnlem  46615  hoidmvval0b  46901  hoidmvlelem2  46907  hoidmvlelem3  46908  hoidmvle  46911  ovnhoi  46914  hoiqssbl  46936  hspmbllem2  46938  vonioo  46993  vonicc  46996  zlidlring  48547  uzlidlring  48548  ovmpordxf  48652  lincop  48721  lincval  48722  lincsum  48742  lincscm  48743  lmod1lem2  48801  lmod1lem3  48802  lmod1lem4  48803  ldepsnlinc  48821  lines  49044  line  49045  rrxlines  49046  rrxline  49047  spheres  49059  fvconstr  49174  fvconstrn0  49175  fvconstr2  49176  catprs  49323  sectrcl2  49335  invrcl2  49337  invfn  49342  isorcl2  49346  sectpropdlem  49348  invpropdlem  49350  isopropdlem  49352  cicpropdlem  49361  iinfconstbas  49378  nelsubclem  49379  nelsubc3lem  49382  ssccatid  49384  resccatlem  49385  cofu2a  49407  cofid2a  49425  cofid2  49427  cofidf2a  49429  cofidf2  49432  oppf2  49452  upfval  49488  upfval2  49489  upfval3  49490  upeu3  49507  upeu4  49508  oppcup3  49521  natoppfb  49543  swapfval  49574  swapf2a  49583  1stfpropd  49602  2ndfpropd  49603  cofuswapf2  49607  tposcurf12  49610  tposcurf2  49612  tposcurf2cl  49614  fucofvalg  49630  fuco11b  49649  fuco23a  49664  precofval3  49683  prcofpropd  49691  catcrcl2  49708  opf12  49716  fucoppcco  49721  thincmod  49742  isthincd2lem2  49747  isthincd  49748  dfinito4  49813  mndtcco2  49898  mndtccatid  49899  oppgoppchom  49902  oppgoppcco  49903  grptcmon  49905  grptcepi  49906  2arwcatlem2  49908  2arwcatlem3  49909  2arwcatlem4  49910  2arwcat  49912  lanrcl  49933  ranrcl  49934  rellan  49935  relran  49936  concom  49975  coccom  49976