Theorem oveqd 7325

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

Syntax hints:   → wi 4   = wceq 1538  (class class class)co 7308

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1968  ax-7 2008  ax-8 2105  ax-9 2113  ax-ext 2706

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1541  df-ex 1779  df-sb 2065  df-clab 2713  df-cleq 2727  df-clel 2813  df-v 3438  df-in 3898  df-ss 3908  df-uni 4844  df-br 5081  df-iota 6410  df-fv 6466  df-ov 7311

This theorem is referenced by:  oveq123d  7329  oveqdr  7336  csbov  7351  csbov12g  7352  ovmpodxf  7456  oprssov  7474  2mpo0  7551  ofeqd  7568  mptmpoopabbrd  7957  mptmpoopabovd  7958  mptmpoopabbrdOLD  7959  mptmpoopabovdOLD  7960  el2mpocsbcl  7961  fnmpoovd  7963  frecseq123  8133  ruclem1  15999  vdwapval  16733  vdwapid1  16735  vdwmc2  16739  vdwpc  16740  vdwlem5  16745  vdwlem8  16748  vdwlem13  16753  prdsval  17225  prdsdsval2  17254  pwsplusgval  17260  pwsmulrval  17261  pwsvscafval  17264  imasval  17281  iscat  17440  iscatd  17441  catidex  17442  catideu  17443  cidfval  17444  cidval  17445  catidd  17448  iscatd2  17449  catlid  17451  catrid  17452  homffval  17458  homfeqd  17463  homfeqval  17465  comfffval  17466  comffval  17467  comfeq  17474  comfeqd  17475  comfeqval  17476  catpropd  17477  oppcval  17481  oppcco  17486  monfval  17503  ismon  17504  oppcmon  17509  oppcepi  17510  sectffval  17521  sectfval  17522  invffval  17529  isoval  17536  dfiso2  17543  isofn  17546  invisoinvl  17561  invcoisoid  17563  isocoinvid  17564  issubc  17609  issubc3  17623  isfunc  17638  cofuval  17656  cofuval2  17661  funcres  17670  funcres2b  17671  funcres2  17672  funcres2c  17676  isfull  17685  isfth  17689  fullres2c  17714  natfval  17721  isnat  17722  fucval  17734  fucco  17739  fucpropd  17754  initoval  17767  termoval  17768  homarcl  17802  coafval  17838  resssetc  17866  resscatc  17883  catciso  17885  xpcval  17953  1stfval  17967  2ndfval  17970  prfval  17975  prfcl  17979  evlfval  17994  curfval  18000  curf1cl  18005  curfcl  18009  uncf1  18013  uncf2  18014  diag12  18021  diag2  18022  curf2ndf  18024  hofval  18029  hof1  18031  hof2fval  18032  hofcl  18036  yon12  18042  yon2  18043  hofpropd  18044  joinval  18154  meetval  18168  isdlat  18299  plusffval  18391  issstrmgm  18396  grpidval  18404  grpidd  18414  gsumvalx  18419  gsumpropd  18421  gsumress  18425  ismndd  18466  issubmnd  18471  submnd0  18473  ismhm  18491  issubm  18501  resmhm  18518  resmhm2  18519  resmhm2b  18520  isgrp  18642  isgrpd2e  18657  grpidd2  18676  grpinvfval  18677  grpinvfvalALT  18678  imasgrp2  18749  imasgrp  18750  subg0  18820  subginv  18821  subgcl  18824  issubgrpd2  18830  isnsg  18842  isghm  18893  resghm  18909  isga  18956  subgga  18965  gasubg  18967  cntzfval  18985  resscntz  18997  odfval  19199  odfvalALT  19200  gexval  19242  lsmfval  19302  lsmvalx  19303  oppglsm  19306  subglsm  19338  pj1fval  19359  efgtval  19388  iscmn  19453  iscmnd  19458  submcmn2  19499  iscyg  19538  cycsubmcmn  19548  issrg  19802  isring  19846  ringidss  19875  prdsmgp  19908  mulgass3  19938  dvdsrval  19946  isirred  20000  isdrngd  20079  isdrngrd  20080  subrg1  20097  subrgmcl  20099  subrgdvds  20101  subrguss  20102  subrginv  20103  subrgdv  20104  subrgunit  20105  subrgugrp  20106  abvfval  20141  isabvd  20143  issrngd  20184  islmod  20190  islmodd  20192  scaffval  20204  lmodpropd  20249  lssset  20258  islssd  20260  prdslmodd  20294  islmhm  20352  reslmhm  20377  reslmhm2  20378  reslmhm2b  20379  islbs  20401  rlmvneg  20541  rrgval  20621  isphl  20896  ipffval  20916  isphld  20922  phssipval  20925  phssip  20926  phlssphl  20927  ocvfval  20934  isobs  20990  frlmplusgval  21034  frlmsubgval  21035  frlmvscafval  21036  frlmip  21048  frlmipval  21049  frlmup1  21068  lsslindf  21100  isassa  21126  isassad  21134  assamulgscmlem2  21167  psrval  21181  resspsradd  21248  resspsrmul  21249  resspsrvsca  21250  mplmon2mul  21340  ply1coe  21530  lply1binomsc  21541  evl1expd  21574  evl1scvarpw  21592  mamufval  21597  matplusg2  21639  matvsca2  21640  matplusgcell  21645  matsubgcell  21646  matinvgcell  21647  matvscacell  21648  matmulcell  21657  mpomatmul  21658  mat1  21659  mattposm  21671  mat1dimmul  21688  dmatmul  21709  dmatcrng  21714  scmataddcl  21728  scmatsubcl  21729  scmatcrng  21733  smatvscl  21736  scmatghm  21745  scmatmhm  21746  mvmulfval  21754  ma1repveval  21783  mdetrlin  21814  mdetrsca  21815  mdetmul  21835  madurid  21856  minmar1cl  21863  smadiadetglem1  21883  smadiadetr  21887  matinv  21889  slesolinv  21892  slesolinvbi  21893  cramerimplem3  21897  cpmatacl  21928  mat2pmatghm  21942  decpmatmullem  21983  decpmatmul  21984  pmatcollpw1lem1  21986  pmatcollpw2lem  21989  pmatcollpwlem  21992  pmatcollpw3lem  21995  mply1topmatval  22016  mp2pm2mplem1  22018  mp2pm2mplem4  22021  mp2pm2mplem5  22022  mp2pm2mp  22023  chpmat1d  22048  chpscmatgsummon  22057  chfacfpmmulgsum2  22077  xkocnv  23028  submtmd  23318  prdsdsf  23583  ressprdsds  23587  blfvalps  23599  prdsxmslem2  23748  tmsxpsval  23757  ngpds  23823  sgrimval  23851  subgngp  23854  tngngp  23881  tngngp3  23883  isnlm  23902  lssnlm  23928  isphtpy  24207  isphtpc  24220  pi1cpbl  24270  pi1addf  24273  pi1addval  24274  pi1grplem  24275  clmsub  24306  clmvsass  24315  clmvsdir  24317  isclmp  24323  cvsdiv  24358  iscph  24397  cphdir  24432  cphdi  24433  cph2di  24434  cph2subdi  24437  cphass  24438  tcphval  24445  ipcau2  24461  tcphcphlem1  24462  tcphcphlem2  24463  cphsscph  24478  caufval  24502  rrxip  24617  rrxvsca  24621  rrxplusgvscavalb  24622  rrxdsfival  24640  ehleudisval  24646  dvlip2  25222  q1pval  25381  r1pval  25384  dvntaylp  25593  efabl  25769  efsubm  25770  dchrmul  26459  istrkgc  26913  istrkgb  26914  istrkgcb  26915  istrkge  26916  istrkgl  26917  istrkgld  26918  iscgrg  26971  isismt  26993  tglngval  27010  legval  27043  ishlg  27061  mirval  27114  israg  27156  ishpg  27218  lmif  27244  islmib  27246  isinag  27297  ttgval  27334  ttgvalOLD  27335  wksonproplem  28170  wksonproplemOLD  28171  wspthsnon  28315  iswwlksnon  28316  iswspthsnon  28319  isconngr  28651  isconngr1  28652  grpodivval  28995  dipfval  29162  ipval  29163  sspgval  29189  sspsval  29191  lnoval  29212  ajfval  29269  dipdir  29302  dipass  29305  htth  29378  isomnd  31425  submomnd  31434  inftmrel  31532  isinftm  31533  isslmd  31553  rngurd  31580  rdivmuldivd  31586  isorng  31596  suborng  31612  resv1r  31635  lsmidllsp  31683  idlinsubrg  31703  prmidlval  31707  idlsrgval  31743  idlsrg0g  31746  rprmval  31759  ply1chr  31764  drgextlsp  31777  fedgmullem1  31806  fedgmullem2  31807  fedgmul  31808  extdg1id  31834  smatlem  31843  submatminr1  31856  metidval  31936  pstmval  31941  pstmfval  31942  zlm0  32006  zlm1  32007  sitmval  32412  breprexp  32709  istrkg2d  32742  afsval  32747  mclsrcl  33619  mppsval  33630  bj-endval  35544  matunitlindflem2  35832  istotbnd  35985  isbnd  35996  rrnequiv  36051  isrngo  36113  rngohomval  36180  idlval  36229  pridlval  36249  lflset  37283  islfld  37286  ldualvadd  37353  ldualsmul  37359  ldualvs  37361  isopos  37404  cmtfvalN  37434  iscvlat  37547  ishlat1  37576  lineset  37962  psubspset  37968  paddfval  38021  paddval  38022  ltrnfset  38341  trnfsetN  38379  trlfset  38384  tgrpov  38972  erngplus  39027  erngmul  39030  erngplus-rN  39035  erngmul-rN  39038  erngdvlem3  39214  erngdvlem4  39215  erng0g  39218  erngdvlem3-rN  39222  erngdvlem4-rN  39223  dvaplusg  39233  dvamulr  39236  dvavadd  39239  dvavsca  39241  dvalveclem  39249  dvhmulr  39310  dvhfvadd  39315  dvhvadd  39316  dvhopvadd2  39318  dvhvaddcl  39319  dvhvaddcomN  39320  dvhvsca  39325  dvhlveclem  39332  dvh0g  39335  djavalN  39359  diblsmopel  39395  dicvaddcl  39414  cdlemn6  39426  dihffval  39454  dihopelvalcpre  39472  djhval  39622  lcdvaddval  39822  lcdsmul  39826  lcdvsval  39828  lcdlkreq2N  39847  hvmapffval  39982  hvmapfval  39983  hdmap1fval  40020  hgmapffval  40109  hgmapfval  40110  hgmapadd  40118  hlhilipval  40177  hlhilhillem  40188  mhphf  40493  mhphf2  40494  prjspval  40650  prjspner1  40671  mnringvald  42052  ioorrnopnlem  44087  hoidmvval0b  44371  hoidmvlelem2  44377  hoidmvlelem3  44378  hoidmvle  44381  ovnhoi  44384  hoiqssbl  44406  hspmbllem2  44408  vonioo  44463  vonicc  44466  ismgmd  45587  ismgmhm  45594  issubmgm  45600  resmgmhm  45609  resmgmhm2  45610  resmgmhm2b  45611  idfusubc  45681  rnghmval  45706  lidlmsgrp  45741  lidlrng  45742  zlidlring  45743  uzlidlring  45744  rnghmresel  45779  rngchom  45782  rngcco  45786  rnghmsubcsetclem1  45790  rhmresel  45825  ringchom  45828  ringcco  45832  rhmsubcsetclem1  45836  rhmsubcrngclem1  45842  irinitoringc  45884  ovmpordxf  45931  lincop  46006  lincval  46007  lincsum  46027  lincscm  46028  lmod1lem2  46086  lmod1lem3  46087  lmod1lem4  46088  ldepsnlinc  46106  lines  46334  line  46335  rrxlines  46336  rrxline  46337  spheres  46349  fvconstr  46440  fvconstrn0  46441  fvconstr2  46442  catprs  46549  thincmod  46569  isthincd2lem2  46574  isthincd  46575  mndtcco2  46630  mndtccatid  46631  grptcmon  46634  grptcepi  46635