Theorem oveqd 7415

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

Syntax hints:   → wi 4   = wceq 1562  (class class class)co 7398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-ss 3923  df-uni 4868  df-br 5103  df-iota 6479  df-fv 6531  df-ov 7401

This theorem is referenced by:  oveq123d  7419  oveqdr  7426  csbov  7443  csbov12g  7444  ovmpodxf  7548  oprssov  7567  2mpo0  7647  ofeqd  7664  mptmpoopabbrd  8064  mptmpoopabovd  8065  el2mpocsbcl  8066  fnmpoovd  8068  frecseq123  8265  ruclem1  16265  vdwapval  17011  vdwapid1  17013  vdwmc2  17017  vdwpc  17018  vdwlem5  17023  vdwlem8  17026  vdwlem13  17031  prdsval  17486  prdsdsval2  17515  pwsplusgval  17522  pwsmulrval  17523  pwsvscafval  17526  imasval  17543  iscat  17706  iscatd  17707  catidex  17708  catideu  17709  cidfval  17710  cidval  17711  catidd  17714  iscatd2  17715  catlid  17717  catrid  17718  homffval  17724  homfeqd  17729  homfeqval  17731  comfffval  17732  comffval  17733  comfeq  17740  comfeqd  17741  comfeqval  17742  catpropd  17743  oppcval  17747  oppcco  17751  monfval  17767  ismon  17768  oppcmon  17773  oppcepi  17774  sectffval  17785  sectfval  17786  invffval  17793  isoval  17800  dfiso2  17807  isofn  17810  invisoinvl  17825  invcoisoid  17827  isocoinvid  17828  issubc  17870  issubc3  17884  isfunc  17899  cofuval  17917  cofuval2  17922  funcres  17931  funcres2b  17932  funcres2  17933  idfusubc  17935  funcres2c  17938  isfull  17947  isfth  17951  fullres2c  17976  natfval  17984  isnat  17985  fucval  17996  fucco  18000  fucpropd  18015  initoval  18028  termoval  18029  homarcl  18063  coafval  18099  resssetc  18127  resscatc  18144  catciso  18146  xpcval  18211  1stfval  18225  2ndfval  18228  prfval  18233  prfcl  18237  evlfval  18251  curfval  18257  curf1cl  18262  curfcl  18266  uncf1  18270  uncf2  18271  diag12  18278  diag2  18279  curf2ndf  18281  hofval  18286  hof1  18288  hof2fval  18289  hofcl  18293  yon12  18299  yon2  18300  hofpropd  18301  joinval  18409  meetval  18423  isdlat  18556  plusffval  18682  ismgmd  18688  issstrmgm  18689  grpidval  18697  grpidd  18707  gsumvalx  18712  gsumpropd  18714  gsumress  18718  ismgmhm  18732  issubmgm  18738  resmgmhm  18747  resmgmhm2  18748  resmgmhm2b  18749  issgrpd  18766  ismndd  18792  issubmnd  18797  submnd0  18799  ismhm  18821  issubm  18839  resmhm  18856  resmhm2  18857  resmhm2b  18858  mhmimalem  18860  isgrp  18983  isgrpd2e  18999  grpidd2  19021  grpinvfval  19022  grpinvfvalALT  19023  imasgrp2  19099  imasgrp  19100  subg0  19176  subginv  19177  subgcl  19180  issubgrpd2  19186  isnsg  19198  isghm  19258  resghm  19274  isga  19333  subgga  19342  gasubg  19344  cntzfval  19362  resscntz  19375  odfval  19574  odfvalALT  19575  gexval  19620  lsmfval  19680  lsmvalx  19681  oppglsm  19684  subglsm  19715  pj1fval  19736  efgtval  19765  iscmn  19831  iscmnd  19836  submcmn2  19881  imasabl  19918  iscyg  19921  cycsubmcmn  19931  isomnd  20165  submomnd  20174  prdsmgp  20199  rngpropd  20222  ringurd  20237  issrg  20240  isring  20289  ringidss  20329  mulgass3  20404  dvdsrval  20412  rdivmuldivd  20464  isirred  20470  rnghmval  20491  islring  20592  lringuplu  20596  subrngmcl  20609  subrg1  20634  subrgdvds  20638  subrguss  20639  subrginv  20640  subrgdv  20641  subrgunit  20642  subrgugrp  20643  rnghmresel  20672  rngchom  20675  rngcco  20679  rnghmsubcsetclem1  20683  rhmresel  20701  ringchom  20704  ringcco  20708  rhmsubcsetclem1  20712  rhmsubcrngclem1  20718  rrgval  20749  isdrngd  20817  isdrngrd  20818  isdrngdOLD  20819  isdrngrdOLD  20820  abvfval  20861  isabvd  20863  issrngd  20906  isorng  20912  suborng  20927  islmod  20933  islmodd  20935  scaffval  20949  lmodpropd  20994  lssset  21002  islssd  21004  prdslmodd  21038  islmhm  21096  reslmhm  21121  reslmhm2  21122  reslmhm2b  21123  islbs  21145  rlmvneg  21275  rnglidlmmgm  21317  rnglidlmsgrp  21318  rnglidlrng  21319  rngqiprngghmlem3  21361  rngqiprngimfolem  21362  rngqiprnglinlem1  21363  rngqiprngimf1  21372  rngqiprnglin  21374  rng2idl1cntr  21377  rngqiprngfulem5  21387  irinitoringc  21533  isphl  21682  ipffval  21702  isphld  21708  phssipval  21711  phssip  21712  phlssphl  21713  ocvfval  21720  isobs  21774  frlmplusgval  21818  frlmsubgval  21819  frlmvscafval  21820  frlmip  21832  frlmipval  21833  frlmup1  21852  lsslindf  21884  isassa  21910  isassad  21919  sraassab  21922  assamulgscmlem2  21954  psrval  21969  resspsradd  22028  resspsrmul  22029  resspsrvsca  22030  mplmon2mul  22124  selvvvval  22197  ply1coe  22363  ply1chr  22371  lply1binomsc  22376  evl1expd  22410  evl1scvarpw  22428  asclply1subcl  22439  mamufval  22454  matplusg2  22489  matvsca2  22490  matplusgcell  22495  matsubgcell  22496  matinvgcell  22497  matvscacell  22498  matmulcell  22507  mpomatmul  22508  mat1  22509  mattposm  22521  mat1dimmul  22538  dmatmul  22559  dmatcrng  22564  scmataddcl  22578  scmatsubcl  22579  scmatcrng  22583  smatvscl  22586  scmatghm  22595  scmatmhm  22596  mvmulfval  22604  ma1repveval  22633  mdetrlin  22664  mdetrsca  22665  mdetmul  22685  madurid  22706  minmar1cl  22713  smadiadetglem1  22733  smadiadetr  22737  matinv  22739  slesolinv  22742  slesolinvbi  22743  cramerimplem3  22747  cpmatacl  22778  mat2pmatghm  22792  decpmatmullem  22833  decpmatmul  22834  pmatcollpw1lem1  22836  pmatcollpw2lem  22839  pmatcollpwlem  22842  pmatcollpw3lem  22845  mply1topmatval  22866  mp2pm2mplem1  22868  mp2pm2mplem4  22871  mp2pm2mplem5  22872  mp2pm2mp  22873  chpmat1d  22898  chpscmatgsummon  22907  chfacfpmmulgsum2  22927  xkocnv  23876  submtmd  24166  prdsdsf  24429  ressprdsds  24433  blfvalps  24445  prdsxmslem2  24591  tmsxpsval  24600  ngpds  24666  sgrimval  24694  subgngp  24697  tngngp  24716  tngngp3  24718  isnlm  24737  lssnlm  24763  isphtpy  25045  isphtpc  25058  pi1cpbl  25108  pi1addf  25111  pi1addval  25112  pi1grplem  25113  clmsub  25144  clmvsass  25153  clmvsdir  25155  isclmp  25161  cvsdiv  25196  iscph  25234  cphdir  25269  cphdi  25270  cph2di  25271  cph2subdi  25274  cphass  25275  tcphval  25282  ipcau2  25298  tcphcphlem1  25299  tcphcphlem2  25300  cphsscph  25315  caufval  25339  rrxip  25454  rrxvsca  25458  rrxplusgvscavalb  25459  rrxdsfival  25477  ehleudisval  25483  dvlip2  26059  q1pval  26217  r1pval  26220  dvntaylp  26436  efabl  26617  efsubm  26618  dchrmul  27314  seqseq123d  28381  istrkgc  28625  istrkgb  28626  istrkgcb  28627  istrkge  28628  istrkgl  28629  istrkgld  28630  iscgrg  28683  isismt  28705  tglngval  28722  legval  28755  ishlg  28773  mirval  28830  israg  28872  ishpg  28934  lmif  28960  islmib  28962  tgplnfn  28984  plngval  28986  isplng  28987  isinag  29034  ttgval  29077  wksonproplem  29905  wspthsnon  30054  iswwlksnon  30055  iswspthsnon  30058  isconngr  30393  isconngr1  30394  grpodivval  30740  dipfval  30907  ipval  30908  sspgval  30934  sspsval  30936  lnoval  30957  ajfval  31014  dipdir  31047  dipass  31050  htth  31123  ressmulgnn0d  33226  inftmrel  33362  isinftm  33363  isslmd  33384  elrgspnlem1  33425  erlval  33441  rlocval  33442  rlocaddval  33452  rlocmulval  33453  subrdom  33471  resv1r  33527  lsmidllsp  33588  idlinsubrg  33619  prmidlval  33625  idlsrgval  33701  idlsrg0g  33704  rprmval  33714  ressply1evls1  33763  vietalem  33878  drgextlsp  33893  fedgmullem1  33928  fedgmullem2  33929  fedgmul  33930  extdg1id  33965  fldextrspunlsplem  33972  fldextrspunlsp  33973  extdgfialglem1  33991  extdgfialglem2  33992  algextdeglem8  34023  smatlem  34096  submatminr1  34109  metidval  34189  pstmval  34194  pstmfval  34195  zlm0  34259  zlm1  34260  sitmval  34648  breprexp  34929  istrkg2d  34962  afsval  34970  mclsrcl  35916  mppsval  35927  bj-endval  37812  matunitlindflem2  38121  istotbnd  38273  isbnd  38284  rrnequiv  38339  isrngo  38401  rngohomval  38468  idlval  38517  pridlval  38537  lflset  39688  islfld  39691  ldualvadd  39758  ldualsmul  39764  ldualvs  39766  isopos  39809  cmtfvalN  39839  iscvlat  39952  ishlat1  39981  lineset  40367  psubspset  40373  paddfval  40426  paddval  40427  ltrnfset  40746  trnfsetN  40784  trlfset  40789  tgrpov  41377  erngplus  41432  erngmul  41435  erngplus-rN  41440  erngmul-rN  41443  erngdvlem3  41619  erngdvlem4  41620  erng0g  41623  erngdvlem3-rN  41627  erngdvlem4-rN  41628  dvaplusg  41638  dvamulr  41641  dvavadd  41644  dvavsca  41646  dvalveclem  41654  dvhmulr  41715  dvhfvadd  41720  dvhvadd  41721  dvhopvadd2  41723  dvhvaddcl  41724  dvhvaddcomN  41725  dvhvsca  41730  dvhlveclem  41737  dvh0g  41740  djavalN  41764  diblsmopel  41800  dicvaddcl  41819  cdlemn6  41831  dihffval  41859  dihopelvalcpre  41877  djhval  42027  lcdvaddval  42227  lcdsmul  42231  lcdvsval  42233  lcdlkreq2N  42252  hvmapffval  42387  hvmapfval  42388  hdmap1fval  42425  hgmapffval  42514  hgmapfval  42515  hgmapadd  42523  hlhilipval  42578  hlhilhillem  42589  isprimroot  42715  aks6d1c1p4  42733  idomnnzpownz  42754  aks6d1c5lem1  42758  aks6d1c5lem3  42759  aks6d1c5lem2  42760  aks5lem3a  42811  unitscyglem5  42821  rhmpsr1  43171  mhphf2  43185  prjspval  43190  prjspner1  43213  sn-isghm  43260  mnringvald  44794  ioorrnopnlem  46883  hoidmvval0b  47169  hoidmvlelem2  47175  hoidmvlelem3  47176  hoidmvle  47179  ovnhoi  47182  hoiqssbl  47204  hspmbllem2  47206  vonioo  47261  vonicc  47264  zlidlring  48861  uzlidlring  48862  ovmpordxf  48966  lincop  49035  lincval  49036  lincsum  49056  lincscm  49057  lmod1lem2  49115  lmod1lem3  49116  lmod1lem4  49117  ldepsnlinc  49135  lines  49358  line  49359  rrxlines  49360  rrxline  49361  spheres  49373  fvconstr  49488  fvconstrn0  49489  fvconstr2  49490  catprs  49637  sectrcl2  49649  invrcl2  49651  invfn  49656  isorcl2  49660  sectpropdlem  49662  invpropdlem  49664  isopropdlem  49666  cicpropdlem  49675  iinfconstbas  49692  nelsubclem  49693  nelsubc3lem  49696  ssccatid  49698  resccatlem  49699  cofu2a  49721  cofid2a  49739  cofid2  49741  cofidf2a  49743  cofidf2  49746  oppf2  49766  upfval  49802  upfval2  49803  upfval3  49804  upeu3  49821  upeu4  49822  oppcup3  49835  natoppfb  49857  swapfval  49888  swapf2a  49897  1stfpropd  49916  2ndfpropd  49917  cofuswapf2  49921  tposcurf12  49924  tposcurf2  49926  tposcurf2cl  49928  fucofvalg  49944  fuco11b  49963  fuco23a  49978  precofval3  49997  prcofpropd  50005  catcrcl2  50022  opf12  50030  fucoppcco  50035  thincmod  50056  isthincd2lem2  50061  isthincd  50062  dfinito4  50127  mndtcco2  50212  mndtccatid  50213  oppgoppchom  50216  oppgoppcco  50217  grptcmon  50219  grptcepi  50220  2arwcatlem2  50222  2arwcatlem3  50223  2arwcatlem4  50224  2arwcat  50226  lanrcl  50247  ranrcl  50248  rellan  50249  relran  50250  concom  50289  coccom  50290