Theorem oveqd 7423

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965  df-uni 4909  df-br 5149  df-iota 6493  df-fv 6549  df-ov 7409

This theorem is referenced by:  oveq123d  7427  oveqdr  7434  csbov  7449  csbov12g  7450  ovmpodxf  7555  oprssov  7573  2mpo0  7652  ofeqd  7669  mptmpoopabbrd  8064  mptmpoopabovd  8065  mptmpoopabbrdOLD  8066  mptmpoopabovdOLD  8067  el2mpocsbcl  8068  fnmpoovd  8070  frecseq123  8264  ruclem1  16171  vdwapval  16903  vdwapid1  16905  vdwmc2  16909  vdwpc  16910  vdwlem5  16915  vdwlem8  16918  vdwlem13  16923  prdsval  17398  prdsdsval2  17427  pwsplusgval  17433  pwsmulrval  17434  pwsvscafval  17437  imasval  17454  iscat  17613  iscatd  17614  catidex  17615  catideu  17616  cidfval  17617  cidval  17618  catidd  17621  iscatd2  17622  catlid  17624  catrid  17625  homffval  17631  homfeqd  17636  homfeqval  17638  comfffval  17639  comffval  17640  comfeq  17647  comfeqd  17648  comfeqval  17649  catpropd  17650  oppcval  17654  oppcco  17659  monfval  17676  ismon  17677  oppcmon  17682  oppcepi  17683  sectffval  17694  sectfval  17695  invffval  17702  isoval  17709  dfiso2  17716  isofn  17719  invisoinvl  17734  invcoisoid  17736  isocoinvid  17737  issubc  17782  issubc3  17796  isfunc  17811  cofuval  17829  cofuval2  17834  funcres  17843  funcres2b  17844  funcres2  17845  funcres2c  17849  isfull  17858  isfth  17862  fullres2c  17887  natfval  17894  isnat  17895  fucval  17907  fucco  17912  fucpropd  17927  initoval  17940  termoval  17941  homarcl  17975  coafval  18011  resssetc  18039  resscatc  18056  catciso  18058  xpcval  18126  1stfval  18140  2ndfval  18143  prfval  18148  prfcl  18152  evlfval  18167  curfval  18173  curf1cl  18178  curfcl  18182  uncf1  18186  uncf2  18187  diag12  18194  diag2  18195  curf2ndf  18197  hofval  18202  hof1  18204  hof2fval  18205  hofcl  18209  yon12  18215  yon2  18216  hofpropd  18217  joinval  18327  meetval  18341  isdlat  18472  plusffval  18564  issstrmgm  18569  grpidval  18577  grpidd  18587  gsumvalx  18592  gsumpropd  18594  gsumress  18598  issgrpd  18618  ismndd  18644  issubmnd  18649  submnd0  18651  ismhm  18670  issubm  18681  resmhm  18698  resmhm2  18699  resmhm2b  18700  mhmimalem  18702  isgrp  18822  isgrpd2e  18838  grpidd2  18859  grpinvfval  18860  grpinvfvalALT  18861  imasgrp2  18935  imasgrp  18936  subg0  19007  subginv  19008  subgcl  19011  issubgrpd2  19017  isnsg  19030  isghm  19087  resghm  19103  isga  19150  subgga  19159  gasubg  19161  cntzfval  19179  resscntz  19192  odfval  19395  odfvalALT  19396  gexval  19441  lsmfval  19501  lsmvalx  19502  oppglsm  19505  subglsm  19536  pj1fval  19557  efgtval  19586  iscmn  19652  iscmnd  19657  submcmn2  19702  imasabl  19739  iscyg  19742  cycsubmcmn  19752  issrg  20005  isring  20054  ringidss  20088  prdsmgp  20126  mulgass3  20160  dvdsrval  20168  rdivmuldivd  20220  isirred  20226  islring  20303  lringuplu  20307  isdrngd  20341  isdrngrd  20342  isdrngdOLD  20343  isdrngrdOLD  20344  subrg1  20366  subrgmcl  20368  subrgdvds  20370  subrguss  20371  subrginv  20372  subrgdv  20373  subrgunit  20374  subrgugrp  20375  abvfval  20419  isabvd  20421  issrngd  20462  islmod  20468  islmodd  20470  scaffval  20483  lmodpropd  20528  lssset  20537  islssd  20539  prdslmodd  20573  islmhm  20631  reslmhm  20656  reslmhm2  20657  reslmhm2b  20658  islbs  20680  rlmvneg  20823  rrgval  20896  isphl  21173  ipffval  21193  isphld  21199  phssipval  21202  phssip  21203  phlssphl  21204  ocvfval  21211  isobs  21267  frlmplusgval  21311  frlmsubgval  21312  frlmvscafval  21313  frlmip  21325  frlmipval  21326  frlmup1  21345  lsslindf  21377  isassa  21403  isassad  21411  sraassab  21414  assamulgscmlem2  21446  psrval  21460  resspsradd  21528  resspsrmul  21529  resspsrvsca  21530  mplmon2mul  21622  ply1coe  21812  lply1binomsc  21823  evl1expd  21856  evl1scvarpw  21874  mamufval  21879  matplusg2  21921  matvsca2  21922  matplusgcell  21927  matsubgcell  21928  matinvgcell  21929  matvscacell  21930  matmulcell  21939  mpomatmul  21940  mat1  21941  mattposm  21953  mat1dimmul  21970  dmatmul  21991  dmatcrng  21996  scmataddcl  22010  scmatsubcl  22011  scmatcrng  22015  smatvscl  22018  scmatghm  22027  scmatmhm  22028  mvmulfval  22036  ma1repveval  22065  mdetrlin  22096  mdetrsca  22097  mdetmul  22117  madurid  22138  minmar1cl  22145  smadiadetglem1  22165  smadiadetr  22169  matinv  22171  slesolinv  22174  slesolinvbi  22175  cramerimplem3  22179  cpmatacl  22210  mat2pmatghm  22224  decpmatmullem  22265  decpmatmul  22266  pmatcollpw1lem1  22268  pmatcollpw2lem  22271  pmatcollpwlem  22274  pmatcollpw3lem  22277  mply1topmatval  22298  mp2pm2mplem1  22300  mp2pm2mplem4  22303  mp2pm2mplem5  22304  mp2pm2mp  22305  chpmat1d  22330  chpscmatgsummon  22339  chfacfpmmulgsum2  22359  xkocnv  23310  submtmd  23600  prdsdsf  23865  ressprdsds  23869  blfvalps  23881  prdsxmslem2  24030  tmsxpsval  24039  ngpds  24105  sgrimval  24133  subgngp  24136  tngngp  24163  tngngp3  24165  isnlm  24184  lssnlm  24210  isphtpy  24489  isphtpc  24502  pi1cpbl  24552  pi1addf  24555  pi1addval  24556  pi1grplem  24557  clmsub  24588  clmvsass  24597  clmvsdir  24599  isclmp  24605  cvsdiv  24640  iscph  24679  cphdir  24714  cphdi  24715  cph2di  24716  cph2subdi  24719  cphass  24720  tcphval  24727  ipcau2  24743  tcphcphlem1  24744  tcphcphlem2  24745  cphsscph  24760  caufval  24784  rrxip  24899  rrxvsca  24903  rrxplusgvscavalb  24904  rrxdsfival  24922  ehleudisval  24928  dvlip2  25504  q1pval  25663  r1pval  25666  dvntaylp  25875  efabl  26051  efsubm  26052  dchrmul  26741  istrkgc  27695  istrkgb  27696  istrkgcb  27697  istrkge  27698  istrkgl  27699  istrkgld  27700  iscgrg  27753  isismt  27775  tglngval  27792  legval  27825  ishlg  27843  mirval  27896  israg  27938  ishpg  28000  lmif  28026  islmib  28028  isinag  28079  ttgval  28116  ttgvalOLD  28117  wksonproplem  28951  wksonproplemOLD  28952  wspthsnon  29096  iswwlksnon  29097  iswspthsnon  29100  isconngr  29432  isconngr1  29433  grpodivval  29776  dipfval  29943  ipval  29944  sspgval  29970  sspsval  29972  lnoval  29993  ajfval  30050  dipdir  30083  dipass  30086  htth  30159  isomnd  32207  submomnd  32216  inftmrel  32314  isinftm  32315  isslmd  32335  rngurd  32368  isorng  32406  suborng  32422  resv1r  32445  lsmidllsp  32499  idlinsubrg  32538  prmidlval  32544  idlsrgval  32606  idlsrg0g  32609  rprmval  32622  asclply1subcl  32649  ply1chr  32650  drgextlsp  32670  fedgmullem1  32703  fedgmullem2  32704  fedgmul  32705  extdg1id  32731  smatlem  32766  submatminr1  32779  metidval  32859  pstmval  32864  pstmfval  32865  zlm0  32929  zlm1  32930  sitmval  33337  breprexp  33634  istrkg2d  33667  afsval  33672  mclsrcl  34541  mppsval  34552  bj-endval  36185  matunitlindflem2  36474  istotbnd  36626  isbnd  36637  rrnequiv  36692  isrngo  36754  rngohomval  36821  idlval  36870  pridlval  36890  lflset  37918  islfld  37921  ldualvadd  37988  ldualsmul  37994  ldualvs  37996  isopos  38039  cmtfvalN  38069  iscvlat  38182  ishlat1  38211  lineset  38598  psubspset  38604  paddfval  38657  paddval  38658  ltrnfset  38977  trnfsetN  39015  trlfset  39020  tgrpov  39608  erngplus  39663  erngmul  39666  erngplus-rN  39671  erngmul-rN  39674  erngdvlem3  39850  erngdvlem4  39851  erng0g  39854  erngdvlem3-rN  39858  erngdvlem4-rN  39859  dvaplusg  39869  dvamulr  39872  dvavadd  39875  dvavsca  39877  dvalveclem  39885  dvhmulr  39946  dvhfvadd  39951  dvhvadd  39952  dvhopvadd2  39954  dvhvaddcl  39955  dvhvaddcomN  39956  dvhvsca  39961  dvhlveclem  39968  dvh0g  39971  djavalN  39995  diblsmopel  40031  dicvaddcl  40050  cdlemn6  40062  dihffval  40090  dihopelvalcpre  40108  djhval  40258  lcdvaddval  40458  lcdsmul  40462  lcdvsval  40464  lcdlkreq2N  40483  hvmapffval  40618  hvmapfval  40619  hdmap1fval  40656  hgmapffval  40745  hgmapfval  40746  hgmapadd  40754  hlhilipval  40813  hlhilhillem  40824  selvvvval  41155  mhphf2  41168  prjspval  41342  prjspner1  41365  mnringvald  42953  ioorrnopnlem  45007  hoidmvval0b  45293  hoidmvlelem2  45299  hoidmvlelem3  45300  hoidmvle  45303  ovnhoi  45306  hoiqssbl  45328  hspmbllem2  45330  vonioo  45385  vonicc  45388  ismgmd  46533  ismgmhm  46540  issubmgm  46546  resmgmhm  46555  resmgmhm2  46556  resmgmhm2b  46557  idfusubc  46627  rngpropd  46660  rnghmval  46675  subrngmcl  46721  rnglidlmmgm  46739  rnglidlmsgrp  46740  rnglidlrng  46741  rngqiprngghmlem3  46755  rngqiprngimfolem  46756  rngqiprnglinlem1  46757  rngqiprngimf1  46766  rngqiprnglin  46768  rng2idl1cntr  46771  zlidlring  46780  uzlidlring  46781  rnghmresel  46816  rngchom  46819  rngcco  46823  rnghmsubcsetclem1  46827  rhmresel  46862  ringchom  46865  ringcco  46869  rhmsubcsetclem1  46873  rhmsubcrngclem1  46879  irinitoringc  46921  ovmpordxf  46968  lincop  47043  lincval  47044  lincsum  47064  lincscm  47065  lmod1lem2  47123  lmod1lem3  47124  lmod1lem4  47125  ldepsnlinc  47143  lines  47371  line  47372  rrxlines  47373  rrxline  47374  spheres  47386  fvconstr  47476  fvconstrn0  47477  fvconstr2  47478  catprs  47585  thincmod  47605  isthincd2lem2  47610  isthincd  47611  mndtcco2  47666  mndtccatid  47667  grptcmon  47670  grptcepi  47671