Theorem oveqd 7375

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

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

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-v 3441  df-ss 3917  df-uni 4863  df-br 5098  df-iota 6447  df-fv 6499  df-ov 7361

This theorem is referenced by:  oveq123d  7379  oveqdr  7386  csbov  7403  csbov12g  7404  ovmpodxf  7508  oprssov  7527  2mpo0  7607  ofeqd  7624  mptmpoopabbrd  8024  mptmpoopabbrdOLD  8025  mptmpoopabovd  8026  el2mpocsbcl  8027  fnmpoovd  8029  frecseq123  8224  ruclem1  16158  vdwapval  16903  vdwapid1  16905  vdwmc2  16909  vdwpc  16910  vdwlem5  16915  vdwlem8  16918  vdwlem13  16923  prdsval  17377  prdsdsval2  17406  pwsplusgval  17413  pwsmulrval  17414  pwsvscafval  17417  imasval  17434  iscat  17597  iscatd  17598  catidex  17599  catideu  17600  cidfval  17601  cidval  17602  catidd  17605  iscatd2  17606  catlid  17608  catrid  17609  homffval  17615  homfeqd  17620  homfeqval  17622  comfffval  17623  comffval  17624  comfeq  17631  comfeqd  17632  comfeqval  17633  catpropd  17634  oppcval  17638  oppcco  17642  monfval  17658  ismon  17659  oppcmon  17664  oppcepi  17665  sectffval  17676  sectfval  17677  invffval  17684  isoval  17691  dfiso2  17698  isofn  17701  invisoinvl  17716  invcoisoid  17718  isocoinvid  17719  issubc  17761  issubc3  17775  isfunc  17790  cofuval  17808  cofuval2  17813  funcres  17822  funcres2b  17823  funcres2  17824  idfusubc  17826  funcres2c  17829  isfull  17838  isfth  17842  fullres2c  17867  natfval  17875  isnat  17876  fucval  17887  fucco  17891  fucpropd  17906  initoval  17919  termoval  17920  homarcl  17954  coafval  17990  resssetc  18018  resscatc  18035  catciso  18037  xpcval  18102  1stfval  18116  2ndfval  18119  prfval  18124  prfcl  18128  evlfval  18142  curfval  18148  curf1cl  18153  curfcl  18157  uncf1  18161  uncf2  18162  diag12  18169  diag2  18170  curf2ndf  18172  hofval  18177  hof1  18179  hof2fval  18180  hofcl  18184  yon12  18190  yon2  18191  hofpropd  18192  joinval  18300  meetval  18314  isdlat  18447  plusffval  18573  ismgmd  18579  issstrmgm  18580  grpidval  18588  grpidd  18598  gsumvalx  18603  gsumpropd  18605  gsumress  18609  ismgmhm  18623  issubmgm  18629  resmgmhm  18638  resmgmhm2  18639  resmgmhm2b  18640  issgrpd  18657  ismndd  18683  issubmnd  18688  submnd0  18690  ismhm  18712  issubm  18730  resmhm  18747  resmhm2  18748  resmhm2b  18749  mhmimalem  18751  isgrp  18871  isgrpd2e  18887  grpidd2  18909  grpinvfval  18910  grpinvfvalALT  18911  imasgrp2  18987  imasgrp  18988  subg0  19064  subginv  19065  subgcl  19068  issubgrpd2  19074  isnsg  19086  isghm  19146  isghmOLD  19147  resghm  19163  isga  19222  subgga  19231  gasubg  19233  cntzfval  19251  resscntz  19264  odfval  19463  odfvalALT  19464  gexval  19509  lsmfval  19569  lsmvalx  19570  oppglsm  19573  subglsm  19604  pj1fval  19625  efgtval  19654  iscmn  19720  iscmnd  19725  submcmn2  19770  imasabl  19807  iscyg  19810  cycsubmcmn  19820  isomnd  20054  submomnd  20063  prdsmgp  20088  rngpropd  20111  ringurd  20122  issrg  20125  isring  20174  ringidss  20214  mulgass3  20291  dvdsrval  20299  rdivmuldivd  20351  isirred  20357  rnghmval  20378  islring  20475  lringuplu  20479  subrngmcl  20492  subrg1  20517  subrgdvds  20521  subrguss  20522  subrginv  20523  subrgdv  20524  subrgunit  20525  subrgugrp  20526  rnghmresel  20555  rngchom  20558  rngcco  20562  rnghmsubcsetclem1  20566  rhmresel  20584  ringchom  20587  ringcco  20591  rhmsubcsetclem1  20595  rhmsubcrngclem1  20601  rrgval  20632  isdrngd  20700  isdrngrd  20701  isdrngdOLD  20702  isdrngrdOLD  20703  abvfval  20745  isabvd  20747  issrngd  20790  isorng  20796  suborng  20811  islmod  20817  islmodd  20819  scaffval  20833  lmodpropd  20878  lssset  20886  islssd  20888  prdslmodd  20922  islmhm  20981  reslmhm  21006  reslmhm2  21007  reslmhm2b  21008  islbs  21030  rlmvneg  21160  rnglidlmmgm  21202  rnglidlmsgrp  21203  rnglidlrng  21204  rngqiprngghmlem3  21246  rngqiprngimfolem  21247  rngqiprnglinlem1  21248  rngqiprngimf1  21257  rngqiprnglin  21259  rng2idl1cntr  21262  rngqiprngfulem5  21272  irinitoringc  21436  isphl  21585  ipffval  21605  isphld  21611  phssipval  21614  phssip  21615  phlssphl  21616  ocvfval  21623  isobs  21677  frlmplusgval  21721  frlmsubgval  21722  frlmvscafval  21723  frlmip  21735  frlmipval  21736  frlmup1  21755  lsslindf  21787  isassa  21813  isassad  21822  sraassab  21825  assamulgscmlem2  21858  psrval  21873  resspsradd  21932  resspsrmul  21933  resspsrvsca  21934  mplmon2mul  22026  ply1coe  22244  ply1chr  22252  lply1binomsc  22257  evl1expd  22291  evl1scvarpw  22309  asclply1subcl  22320  mamufval  22338  matplusg2  22373  matvsca2  22374  matplusgcell  22379  matsubgcell  22380  matinvgcell  22381  matvscacell  22382  matmulcell  22391  mpomatmul  22392  mat1  22393  mattposm  22405  mat1dimmul  22422  dmatmul  22443  dmatcrng  22448  scmataddcl  22462  scmatsubcl  22463  scmatcrng  22467  smatvscl  22470  scmatghm  22479  scmatmhm  22480  mvmulfval  22488  ma1repveval  22517  mdetrlin  22548  mdetrsca  22549  mdetmul  22569  madurid  22590  minmar1cl  22597  smadiadetglem1  22617  smadiadetr  22621  matinv  22623  slesolinv  22626  slesolinvbi  22627  cramerimplem3  22631  cpmatacl  22662  mat2pmatghm  22676  decpmatmullem  22717  decpmatmul  22718  pmatcollpw1lem1  22720  pmatcollpw2lem  22723  pmatcollpwlem  22726  pmatcollpw3lem  22729  mply1topmatval  22750  mp2pm2mplem1  22752  mp2pm2mplem4  22755  mp2pm2mplem5  22756  mp2pm2mp  22757  chpmat1d  22782  chpscmatgsummon  22791  chfacfpmmulgsum2  22811  xkocnv  23760  submtmd  24050  prdsdsf  24313  ressprdsds  24317  blfvalps  24329  prdsxmslem2  24475  tmsxpsval  24484  ngpds  24550  sgrimval  24578  subgngp  24581  tngngp  24600  tngngp3  24602  isnlm  24621  lssnlm  24647  isphtpy  24938  isphtpc  24951  pi1cpbl  25002  pi1addf  25005  pi1addval  25006  pi1grplem  25007  clmsub  25038  clmvsass  25047  clmvsdir  25049  isclmp  25055  cvsdiv  25090  iscph  25128  cphdir  25163  cphdi  25164  cph2di  25165  cph2subdi  25168  cphass  25169  tcphval  25176  ipcau2  25192  tcphcphlem1  25193  tcphcphlem2  25194  cphsscph  25209  caufval  25233  rrxip  25348  rrxvsca  25352  rrxplusgvscavalb  25353  rrxdsfival  25371  ehleudisval  25377  dvlip2  25958  q1pval  26118  r1pval  26121  dvntaylp  26337  efabl  26517  efsubm  26518  dchrmul  27217  seqseq123d  28265  istrkgc  28507  istrkgb  28508  istrkgcb  28509  istrkge  28510  istrkgl  28511  istrkgld  28512  iscgrg  28565  isismt  28587  tglngval  28604  legval  28637  ishlg  28655  mirval  28708  israg  28750  ishpg  28812  lmif  28838  islmib  28840  isinag  28891  ttgval  28928  wksonproplem  29757  wspthsnon  29906  iswwlksnon  29907  iswspthsnon  29910  isconngr  30245  isconngr1  30246  grpodivval  30591  dipfval  30758  ipval  30759  sspgval  30785  sspsval  30787  lnoval  30808  ajfval  30865  dipdir  30898  dipass  30901  htth  30974  ressmulgnn0d  33106  inftmrel  33241  isinftm  33242  isslmd  33263  elrgspnlem1  33303  erlval  33319  rlocval  33320  rlocaddval  33329  rlocmulval  33330  subrdom  33346  resv1r  33399  lsmidllsp  33460  idlinsubrg  33491  prmidlval  33497  idlsrgval  33563  idlsrg0g  33566  rprmval  33576  ressply1evls1  33625  vietalem  33714  drgextlsp  33729  fedgmullem1  33765  fedgmullem2  33766  fedgmul  33767  extdg1id  33802  fldextrspunlsplem  33809  fldextrspunlsp  33810  extdgfialglem1  33828  extdgfialglem2  33829  algextdeglem8  33860  smatlem  33933  submatminr1  33946  metidval  34026  pstmval  34031  pstmfval  34032  zlm0  34096  zlm1  34097  sitmval  34485  breprexp  34769  istrkg2d  34802  afsval  34807  mclsrcl  35734  mppsval  35745  bj-endval  37489  matunitlindflem2  37787  istotbnd  37939  isbnd  37950  rrnequiv  38005  isrngo  38067  rngohomval  38134  idlval  38183  pridlval  38203  lflset  39354  islfld  39357  ldualvadd  39424  ldualsmul  39430  ldualvs  39432  isopos  39475  cmtfvalN  39505  iscvlat  39618  ishlat1  39647  lineset  40033  psubspset  40039  paddfval  40092  paddval  40093  ltrnfset  40412  trnfsetN  40450  trlfset  40455  tgrpov  41043  erngplus  41098  erngmul  41101  erngplus-rN  41106  erngmul-rN  41109  erngdvlem3  41285  erngdvlem4  41286  erng0g  41289  erngdvlem3-rN  41293  erngdvlem4-rN  41294  dvaplusg  41304  dvamulr  41307  dvavadd  41310  dvavsca  41312  dvalveclem  41320  dvhmulr  41381  dvhfvadd  41386  dvhvadd  41387  dvhopvadd2  41389  dvhvaddcl  41390  dvhvaddcomN  41391  dvhvsca  41396  dvhlveclem  41403  dvh0g  41406  djavalN  41430  diblsmopel  41466  dicvaddcl  41485  cdlemn6  41497  dihffval  41525  dihopelvalcpre  41543  djhval  41693  lcdvaddval  41893  lcdsmul  41897  lcdvsval  41899  lcdlkreq2N  41918  hvmapffval  42053  hvmapfval  42054  hdmap1fval  42091  hgmapffval  42180  hgmapfval  42181  hgmapadd  42189  hlhilipval  42244  hlhilhillem  42255  isprimroot  42382  aks6d1c1p4  42400  idomnnzpownz  42421  aks6d1c5lem1  42425  aks6d1c5lem3  42426  aks6d1c5lem2  42427  aks5lem3a  42478  unitscyglem5  42488  rhmpsr1  42843  selvvvval  42865  mhphf2  42878  prjspval  42883  prjspner1  42906  sn-isghm  42953  mnringvald  44491  ioorrnopnlem  46585  hoidmvval0b  46871  hoidmvlelem2  46877  hoidmvlelem3  46878  hoidmvle  46881  ovnhoi  46884  hoiqssbl  46906  hspmbllem2  46908  vonioo  46963  vonicc  46966  zlidlring  48517  uzlidlring  48518  ovmpordxf  48622  lincop  48691  lincval  48692  lincsum  48712  lincscm  48713  lmod1lem2  48771  lmod1lem3  48772  lmod1lem4  48773  ldepsnlinc  48791  lines  49014  line  49015  rrxlines  49016  rrxline  49017  spheres  49029  fvconstr  49144  fvconstrn0  49145  fvconstr2  49146  catprs  49293  sectrcl2  49305  invrcl2  49307  invfn  49312  isorcl2  49316  sectpropdlem  49318  invpropdlem  49320  isopropdlem  49322  cicpropdlem  49331  iinfconstbas  49348  nelsubclem  49349  nelsubc3lem  49352  ssccatid  49354  resccatlem  49355  cofu2a  49377  cofid2a  49395  cofid2  49397  cofidf2a  49399  cofidf2  49402  oppf2  49422  upfval  49458  upfval2  49459  upfval3  49460  upeu3  49477  upeu4  49478  oppcup3  49491  natoppfb  49513  swapfval  49544  swapf2a  49553  1stfpropd  49572  2ndfpropd  49573  cofuswapf2  49577  tposcurf12  49580  tposcurf2  49582  tposcurf2cl  49584  fucofvalg  49600  fuco11b  49619  fuco23a  49634  precofval3  49653  prcofpropd  49661  catcrcl2  49678  opf12  49686  fucoppcco  49691  thincmod  49712  isthincd2lem2  49717  isthincd  49718  dfinito4  49783  mndtcco2  49868  mndtccatid  49869  oppgoppchom  49872  oppgoppcco  49873  grptcmon  49875  grptcepi  49876  2arwcatlem2  49878  2arwcatlem3  49879  2arwcatlem4  49880  2arwcat  49882  lanrcl  49903  ranrcl  49904  rellan  49905  relran  49906  concom  49945  coccom  49946