Theorem oveqd 7448

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

Syntax hints:   → wi 4   = wceq 1540  (class class class)co 7431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  oveq123d  7452  oveqdr  7459  csbov  7476  csbov12g  7477  ovmpodxf  7583  oprssov  7602  2mpo0  7682  ofeqd  7699  mptmpoopabbrd  8105  mptmpoopabbrdOLD  8106  mptmpoopabovd  8107  mptmpoopabbrdOLDOLD  8108  mptmpoopabovdOLD  8109  el2mpocsbcl  8110  fnmpoovd  8112  frecseq123  8307  ruclem1  16267  vdwapval  17011  vdwapid1  17013  vdwmc2  17017  vdwpc  17018  vdwlem5  17023  vdwlem8  17026  vdwlem13  17031  prdsval  17500  prdsdsval2  17529  pwsplusgval  17535  pwsmulrval  17536  pwsvscafval  17539  imasval  17556  iscat  17715  iscatd  17716  catidex  17717  catideu  17718  cidfval  17719  cidval  17720  catidd  17723  iscatd2  17724  catlid  17726  catrid  17727  homffval  17733  homfeqd  17738  homfeqval  17740  comfffval  17741  comffval  17742  comfeq  17749  comfeqd  17750  comfeqval  17751  catpropd  17752  oppcval  17756  oppcco  17760  monfval  17776  ismon  17777  oppcmon  17782  oppcepi  17783  sectffval  17794  sectfval  17795  invffval  17802  isoval  17809  dfiso2  17816  isofn  17819  invisoinvl  17834  invcoisoid  17836  isocoinvid  17837  issubc  17880  issubc3  17894  isfunc  17909  cofuval  17927  cofuval2  17932  funcres  17941  funcres2b  17942  funcres2  17943  idfusubc  17945  funcres2c  17948  isfull  17957  isfth  17961  fullres2c  17986  natfval  17994  isnat  17995  fucval  18006  fucco  18010  fucpropd  18025  initoval  18038  termoval  18039  homarcl  18073  coafval  18109  resssetc  18137  resscatc  18154  catciso  18156  xpcval  18222  1stfval  18236  2ndfval  18239  prfval  18244  prfcl  18248  evlfval  18262  curfval  18268  curf1cl  18273  curfcl  18277  uncf1  18281  uncf2  18282  diag12  18289  diag2  18290  curf2ndf  18292  hofval  18297  hof1  18299  hof2fval  18300  hofcl  18304  yon12  18310  yon2  18311  hofpropd  18312  joinval  18422  meetval  18436  isdlat  18567  plusffval  18659  ismgmd  18665  issstrmgm  18666  grpidval  18674  grpidd  18684  gsumvalx  18689  gsumpropd  18691  gsumress  18695  ismgmhm  18709  issubmgm  18715  resmgmhm  18724  resmgmhm2  18725  resmgmhm2b  18726  issgrpd  18743  ismndd  18769  issubmnd  18774  submnd0  18776  ismhm  18798  issubm  18816  resmhm  18833  resmhm2  18834  resmhm2b  18835  mhmimalem  18837  isgrp  18957  isgrpd2e  18973  grpidd2  18995  grpinvfval  18996  grpinvfvalALT  18997  imasgrp2  19073  imasgrp  19074  subg0  19150  subginv  19151  subgcl  19154  issubgrpd2  19160  isnsg  19173  isghm  19233  isghmOLD  19234  resghm  19250  isga  19309  subgga  19318  gasubg  19320  cntzfval  19338  resscntz  19351  odfval  19550  odfvalALT  19551  gexval  19596  lsmfval  19656  lsmvalx  19657  oppglsm  19660  subglsm  19691  pj1fval  19712  efgtval  19741  iscmn  19807  iscmnd  19812  submcmn2  19857  imasabl  19894  iscyg  19897  cycsubmcmn  19907  prdsmgp  20148  rngpropd  20171  ringurd  20182  issrg  20185  isring  20234  ringidss  20274  mulgass3  20353  dvdsrval  20361  rdivmuldivd  20413  isirred  20419  rnghmval  20440  islring  20540  lringuplu  20544  subrngmcl  20557  subrg1  20582  subrgdvds  20586  subrguss  20587  subrginv  20588  subrgdv  20589  subrgunit  20590  subrgugrp  20591  rnghmresel  20620  rngchom  20623  rngcco  20627  rnghmsubcsetclem1  20631  rhmresel  20649  ringchom  20652  ringcco  20656  rhmsubcsetclem1  20660  rhmsubcrngclem1  20666  rrgval  20697  isdrngd  20765  isdrngrd  20766  isdrngdOLD  20767  isdrngrdOLD  20768  abvfval  20811  isabvd  20813  issrngd  20856  islmod  20862  islmodd  20864  scaffval  20878  lmodpropd  20923  lssset  20931  islssd  20933  prdslmodd  20967  islmhm  21026  reslmhm  21051  reslmhm2  21052  reslmhm2b  21053  islbs  21075  rlmvneg  21213  rnglidlmmgm  21255  rnglidlmsgrp  21256  rnglidlrng  21257  rngqiprngghmlem3  21299  rngqiprngimfolem  21300  rngqiprnglinlem1  21301  rngqiprngimf1  21310  rngqiprnglin  21312  rng2idl1cntr  21315  rngqiprngfulem5  21325  irinitoringc  21490  isphl  21646  ipffval  21666  isphld  21672  phssipval  21675  phssip  21676  phlssphl  21677  ocvfval  21684  isobs  21740  frlmplusgval  21784  frlmsubgval  21785  frlmvscafval  21786  frlmip  21798  frlmipval  21799  frlmup1  21818  lsslindf  21850  isassa  21876  isassad  21885  sraassab  21888  assamulgscmlem2  21920  psrval  21935  resspsradd  21995  resspsrmul  21996  resspsrvsca  21997  mplmon2mul  22093  ply1coe  22302  ply1chr  22310  lply1binomsc  22315  evl1expd  22349  evl1scvarpw  22367  asclply1subcl  22378  mamufval  22396  matplusg2  22433  matvsca2  22434  matplusgcell  22439  matsubgcell  22440  matinvgcell  22441  matvscacell  22442  matmulcell  22451  mpomatmul  22452  mat1  22453  mattposm  22465  mat1dimmul  22482  dmatmul  22503  dmatcrng  22508  scmataddcl  22522  scmatsubcl  22523  scmatcrng  22527  smatvscl  22530  scmatghm  22539  scmatmhm  22540  mvmulfval  22548  ma1repveval  22577  mdetrlin  22608  mdetrsca  22609  mdetmul  22629  madurid  22650  minmar1cl  22657  smadiadetglem1  22677  smadiadetr  22681  matinv  22683  slesolinv  22686  slesolinvbi  22687  cramerimplem3  22691  cpmatacl  22722  mat2pmatghm  22736  decpmatmullem  22777  decpmatmul  22778  pmatcollpw1lem1  22780  pmatcollpw2lem  22783  pmatcollpwlem  22786  pmatcollpw3lem  22789  mply1topmatval  22810  mp2pm2mplem1  22812  mp2pm2mplem4  22815  mp2pm2mplem5  22816  mp2pm2mp  22817  chpmat1d  22842  chpscmatgsummon  22851  chfacfpmmulgsum2  22871  xkocnv  23822  submtmd  24112  prdsdsf  24377  ressprdsds  24381  blfvalps  24393  prdsxmslem2  24542  tmsxpsval  24551  ngpds  24617  sgrimval  24645  subgngp  24648  tngngp  24675  tngngp3  24677  isnlm  24696  lssnlm  24722  isphtpy  25013  isphtpc  25026  pi1cpbl  25077  pi1addf  25080  pi1addval  25081  pi1grplem  25082  clmsub  25113  clmvsass  25122  clmvsdir  25124  isclmp  25130  cvsdiv  25165  iscph  25204  cphdir  25239  cphdi  25240  cph2di  25241  cph2subdi  25244  cphass  25245  tcphval  25252  ipcau2  25268  tcphcphlem1  25269  tcphcphlem2  25270  cphsscph  25285  caufval  25309  rrxip  25424  rrxvsca  25428  rrxplusgvscavalb  25429  rrxdsfival  25447  ehleudisval  25453  dvlip2  26034  q1pval  26194  r1pval  26197  dvntaylp  26413  efabl  26592  efsubm  26593  dchrmul  27292  seqseq123d  28292  istrkgc  28462  istrkgb  28463  istrkgcb  28464  istrkge  28465  istrkgl  28466  istrkgld  28467  iscgrg  28520  isismt  28542  tglngval  28559  legval  28592  ishlg  28610  mirval  28663  israg  28705  ishpg  28767  lmif  28793  islmib  28795  isinag  28846  ttgval  28883  ttgvalOLD  28884  wksonproplem  29722  wksonproplemOLD  29723  wspthsnon  29872  iswwlksnon  29873  iswspthsnon  29876  isconngr  30208  isconngr1  30209  grpodivval  30554  dipfval  30721  ipval  30722  sspgval  30748  sspsval  30750  lnoval  30771  ajfval  30828  dipdir  30861  dipass  30864  htth  30937  isomnd  33078  submomnd  33087  inftmrel  33187  isinftm  33188  isslmd  33208  elrgspnlem1  33246  erlval  33262  rlocval  33263  rlocaddval  33272  rlocmulval  33273  subrdom  33288  isorng  33329  suborng  33345  resv1r  33368  lsmidllsp  33428  idlinsubrg  33459  prmidlval  33465  idlsrgval  33531  idlsrg0g  33534  rprmval  33544  drgextlsp  33644  fedgmullem1  33680  fedgmullem2  33681  fedgmul  33682  extdg1id  33716  fldextrspunlsplem  33723  fldextrspunlsp  33724  algextdeglem8  33765  smatlem  33796  submatminr1  33809  metidval  33889  pstmval  33894  pstmfval  33895  zlm0  33959  zlm1  33960  sitmval  34351  breprexp  34648  istrkg2d  34681  afsval  34686  mclsrcl  35566  mppsval  35577  bj-endval  37316  matunitlindflem2  37624  istotbnd  37776  isbnd  37787  rrnequiv  37842  isrngo  37904  rngohomval  37971  idlval  38020  pridlval  38040  lflset  39060  islfld  39063  ldualvadd  39130  ldualsmul  39136  ldualvs  39138  isopos  39181  cmtfvalN  39211  iscvlat  39324  ishlat1  39353  lineset  39740  psubspset  39746  paddfval  39799  paddval  39800  ltrnfset  40119  trnfsetN  40157  trlfset  40162  tgrpov  40750  erngplus  40805  erngmul  40808  erngplus-rN  40813  erngmul-rN  40816  erngdvlem3  40992  erngdvlem4  40993  erng0g  40996  erngdvlem3-rN  41000  erngdvlem4-rN  41001  dvaplusg  41011  dvamulr  41014  dvavadd  41017  dvavsca  41019  dvalveclem  41027  dvhmulr  41088  dvhfvadd  41093  dvhvadd  41094  dvhopvadd2  41096  dvhvaddcl  41097  dvhvaddcomN  41098  dvhvsca  41103  dvhlveclem  41110  dvh0g  41113  djavalN  41137  diblsmopel  41173  dicvaddcl  41192  cdlemn6  41204  dihffval  41232  dihopelvalcpre  41250  djhval  41400  lcdvaddval  41600  lcdsmul  41604  lcdvsval  41606  lcdlkreq2N  41625  hvmapffval  41760  hvmapfval  41761  hdmap1fval  41798  hgmapffval  41887  hgmapfval  41888  hgmapadd  41896  hlhilipval  41955  hlhilhillem  41966  isprimroot  42094  aks6d1c1p4  42112  idomnnzpownz  42133  aks6d1c5lem1  42137  aks6d1c5lem3  42138  aks6d1c5lem2  42139  aks5lem3a  42190  unitscyglem5  42200  rhmpsr1  42563  selvvvval  42595  mhphf2  42608  prjspval  42613  prjspner1  42636  sn-isghm  42683  mnringvald  44227  ioorrnopnlem  46319  hoidmvval0b  46605  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvle  46615  ovnhoi  46618  hoiqssbl  46640  hspmbllem2  46642  vonioo  46697  vonicc  46700  zlidlring  48150  uzlidlring  48151  ovmpordxf  48255  lincop  48325  lincval  48326  lincsum  48346  lincscm  48347  lmod1lem2  48405  lmod1lem3  48406  lmod1lem4  48407  ldepsnlinc  48425  lines  48652  line  48653  rrxlines  48654  rrxline  48655  spheres  48667  fvconstr  48765  fvconstrn0  48766  fvconstr2  48767  catprs  48900  upfval  48933  upfval2  48934  upfval3  48935  upeu3  48946  upeu4  48947  swapfval  48968  swapf2a  48977  cofuswapf2  48995  tposcurf12  48998  tposcurf2  49000  tposcurf2cl  49002  fucofvalg  49013  fuco11b  49032  fuco23a  49047  precoffunc  49066  thincmod  49079  isthincd2lem2  49084  isthincd  49085  mndtcco2  49183  mndtccatid  49184  oppgoppchom  49187  oppgoppcco  49188  grptcmon  49190  grptcepi  49191