Theorem oveqd 7366

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352

This theorem is referenced by:  oveq123d  7370  oveqdr  7377  csbov  7394  csbov12g  7395  ovmpodxf  7499  oprssov  7518  2mpo0  7598  ofeqd  7615  mptmpoopabbrd  8015  mptmpoopabbrdOLD  8016  mptmpoopabovd  8017  el2mpocsbcl  8018  fnmpoovd  8020  frecseq123  8215  ruclem1  16140  vdwapval  16885  vdwapid1  16887  vdwmc2  16891  vdwpc  16892  vdwlem5  16897  vdwlem8  16900  vdwlem13  16905  prdsval  17359  prdsdsval2  17388  pwsplusgval  17394  pwsmulrval  17395  pwsvscafval  17398  imasval  17415  iscat  17578  iscatd  17579  catidex  17580  catideu  17581  cidfval  17582  cidval  17583  catidd  17586  iscatd2  17587  catlid  17589  catrid  17590  homffval  17596  homfeqd  17601  homfeqval  17603  comfffval  17604  comffval  17605  comfeq  17612  comfeqd  17613  comfeqval  17614  catpropd  17615  oppcval  17619  oppcco  17623  monfval  17639  ismon  17640  oppcmon  17645  oppcepi  17646  sectffval  17657  sectfval  17658  invffval  17665  isoval  17672  dfiso2  17679  isofn  17682  invisoinvl  17697  invcoisoid  17699  isocoinvid  17700  issubc  17742  issubc3  17756  isfunc  17771  cofuval  17789  cofuval2  17794  funcres  17803  funcres2b  17804  funcres2  17805  idfusubc  17807  funcres2c  17810  isfull  17819  isfth  17823  fullres2c  17848  natfval  17856  isnat  17857  fucval  17868  fucco  17872  fucpropd  17887  initoval  17900  termoval  17901  homarcl  17935  coafval  17971  resssetc  17999  resscatc  18016  catciso  18018  xpcval  18083  1stfval  18097  2ndfval  18100  prfval  18105  prfcl  18109  evlfval  18123  curfval  18129  curf1cl  18134  curfcl  18138  uncf1  18142  uncf2  18143  diag12  18150  diag2  18151  curf2ndf  18153  hofval  18158  hof1  18160  hof2fval  18161  hofcl  18165  yon12  18171  yon2  18172  hofpropd  18173  joinval  18281  meetval  18295  isdlat  18428  plusffval  18520  ismgmd  18526  issstrmgm  18527  grpidval  18535  grpidd  18545  gsumvalx  18550  gsumpropd  18552  gsumress  18556  ismgmhm  18570  issubmgm  18576  resmgmhm  18585  resmgmhm2  18586  resmgmhm2b  18587  issgrpd  18604  ismndd  18630  issubmnd  18635  submnd0  18637  ismhm  18659  issubm  18677  resmhm  18694  resmhm2  18695  resmhm2b  18696  mhmimalem  18698  isgrp  18818  isgrpd2e  18834  grpidd2  18856  grpinvfval  18857  grpinvfvalALT  18858  imasgrp2  18934  imasgrp  18935  subg0  19011  subginv  19012  subgcl  19015  issubgrpd2  19021  isnsg  19034  isghm  19094  isghmOLD  19095  resghm  19111  isga  19170  subgga  19179  gasubg  19181  cntzfval  19199  resscntz  19212  odfval  19411  odfvalALT  19412  gexval  19457  lsmfval  19517  lsmvalx  19518  oppglsm  19521  subglsm  19552  pj1fval  19573  efgtval  19602  iscmn  19668  iscmnd  19673  submcmn2  19718  imasabl  19755  iscyg  19758  cycsubmcmn  19768  isomnd  20002  submomnd  20011  prdsmgp  20036  rngpropd  20059  ringurd  20070  issrg  20073  isring  20122  ringidss  20162  mulgass3  20238  dvdsrval  20246  rdivmuldivd  20298  isirred  20304  rnghmval  20325  islring  20425  lringuplu  20429  subrngmcl  20442  subrg1  20467  subrgdvds  20471  subrguss  20472  subrginv  20473  subrgdv  20474  subrgunit  20475  subrgugrp  20476  rnghmresel  20505  rngchom  20508  rngcco  20512  rnghmsubcsetclem1  20516  rhmresel  20534  ringchom  20537  ringcco  20541  rhmsubcsetclem1  20545  rhmsubcrngclem1  20551  rrgval  20582  isdrngd  20650  isdrngrd  20651  isdrngdOLD  20652  isdrngrdOLD  20653  abvfval  20695  isabvd  20697  issrngd  20740  isorng  20746  suborng  20761  islmod  20767  islmodd  20769  scaffval  20783  lmodpropd  20828  lssset  20836  islssd  20838  prdslmodd  20872  islmhm  20931  reslmhm  20956  reslmhm2  20957  reslmhm2b  20958  islbs  20980  rlmvneg  21110  rnglidlmmgm  21152  rnglidlmsgrp  21153  rnglidlrng  21154  rngqiprngghmlem3  21196  rngqiprngimfolem  21197  rngqiprnglinlem1  21198  rngqiprngimf1  21207  rngqiprnglin  21209  rng2idl1cntr  21212  rngqiprngfulem5  21222  irinitoringc  21386  isphl  21535  ipffval  21555  isphld  21561  phssipval  21564  phssip  21565  phlssphl  21566  ocvfval  21573  isobs  21627  frlmplusgval  21671  frlmsubgval  21672  frlmvscafval  21673  frlmip  21685  frlmipval  21686  frlmup1  21705  lsslindf  21737  isassa  21763  isassad  21772  sraassab  21775  assamulgscmlem2  21807  psrval  21822  resspsradd  21882  resspsrmul  21883  resspsrvsca  21884  mplmon2mul  21974  ply1coe  22183  ply1chr  22191  lply1binomsc  22196  evl1expd  22230  evl1scvarpw  22248  asclply1subcl  22259  mamufval  22277  matplusg2  22312  matvsca2  22313  matplusgcell  22318  matsubgcell  22319  matinvgcell  22320  matvscacell  22321  matmulcell  22330  mpomatmul  22331  mat1  22332  mattposm  22344  mat1dimmul  22361  dmatmul  22382  dmatcrng  22387  scmataddcl  22401  scmatsubcl  22402  scmatcrng  22406  smatvscl  22409  scmatghm  22418  scmatmhm  22419  mvmulfval  22427  ma1repveval  22456  mdetrlin  22487  mdetrsca  22488  mdetmul  22508  madurid  22529  minmar1cl  22536  smadiadetglem1  22556  smadiadetr  22560  matinv  22562  slesolinv  22565  slesolinvbi  22566  cramerimplem3  22570  cpmatacl  22601  mat2pmatghm  22615  decpmatmullem  22656  decpmatmul  22657  pmatcollpw1lem1  22659  pmatcollpw2lem  22662  pmatcollpwlem  22665  pmatcollpw3lem  22668  mply1topmatval  22689  mp2pm2mplem1  22691  mp2pm2mplem4  22694  mp2pm2mplem5  22695  mp2pm2mp  22696  chpmat1d  22721  chpscmatgsummon  22730  chfacfpmmulgsum2  22750  xkocnv  23699  submtmd  23989  prdsdsf  24253  ressprdsds  24257  blfvalps  24269  prdsxmslem2  24415  tmsxpsval  24424  ngpds  24490  sgrimval  24518  subgngp  24521  tngngp  24540  tngngp3  24542  isnlm  24561  lssnlm  24587  isphtpy  24878  isphtpc  24891  pi1cpbl  24942  pi1addf  24945  pi1addval  24946  pi1grplem  24947  clmsub  24978  clmvsass  24987  clmvsdir  24989  isclmp  24995  cvsdiv  25030  iscph  25068  cphdir  25103  cphdi  25104  cph2di  25105  cph2subdi  25108  cphass  25109  tcphval  25116  ipcau2  25132  tcphcphlem1  25133  tcphcphlem2  25134  cphsscph  25149  caufval  25173  rrxip  25288  rrxvsca  25292  rrxplusgvscavalb  25293  rrxdsfival  25311  ehleudisval  25317  dvlip2  25898  q1pval  26058  r1pval  26061  dvntaylp  26277  efabl  26457  efsubm  26458  dchrmul  27157  seqseq123d  28187  istrkgc  28403  istrkgb  28404  istrkgcb  28405  istrkge  28406  istrkgl  28407  istrkgld  28408  iscgrg  28461  isismt  28483  tglngval  28500  legval  28533  ishlg  28551  mirval  28604  israg  28646  ishpg  28708  lmif  28734  islmib  28736  isinag  28787  ttgval  28824  wksonproplem  29652  wspthsnon  29801  iswwlksnon  29802  iswspthsnon  29805  isconngr  30137  isconngr1  30138  grpodivval  30483  dipfval  30650  ipval  30651  sspgval  30677  sspsval  30679  lnoval  30700  ajfval  30757  dipdir  30790  dipass  30793  htth  30866  ressmulgnn0d  33007  inftmrel  33131  isinftm  33132  isslmd  33153  elrgspnlem1  33191  erlval  33207  rlocval  33208  rlocaddval  33217  rlocmulval  33218  subrdom  33233  resv1r  33286  lsmidllsp  33346  idlinsubrg  33377  prmidlval  33383  idlsrgval  33449  idlsrg0g  33452  rprmval  33462  ressply1evls1  33509  drgextlsp  33576  fedgmullem1  33612  fedgmullem2  33613  fedgmul  33614  extdg1id  33649  fldextrspunlsplem  33656  fldextrspunlsp  33657  extdgfialglem1  33675  extdgfialglem2  33676  algextdeglem8  33707  smatlem  33780  submatminr1  33793  metidval  33873  pstmval  33878  pstmfval  33879  zlm0  33943  zlm1  33944  sitmval  34333  breprexp  34617  istrkg2d  34650  afsval  34655  mclsrcl  35554  mppsval  35565  bj-endval  37309  matunitlindflem2  37617  istotbnd  37769  isbnd  37780  rrnequiv  37835  isrngo  37897  rngohomval  37964  idlval  38013  pridlval  38033  lflset  39058  islfld  39061  ldualvadd  39128  ldualsmul  39134  ldualvs  39136  isopos  39179  cmtfvalN  39209  iscvlat  39322  ishlat1  39351  lineset  39737  psubspset  39743  paddfval  39796  paddval  39797  ltrnfset  40116  trnfsetN  40154  trlfset  40159  tgrpov  40747  erngplus  40802  erngmul  40805  erngplus-rN  40810  erngmul-rN  40813  erngdvlem3  40989  erngdvlem4  40990  erng0g  40993  erngdvlem3-rN  40997  erngdvlem4-rN  40998  dvaplusg  41008  dvamulr  41011  dvavadd  41014  dvavsca  41016  dvalveclem  41024  dvhmulr  41085  dvhfvadd  41090  dvhvadd  41091  dvhopvadd2  41093  dvhvaddcl  41094  dvhvaddcomN  41095  dvhvsca  41100  dvhlveclem  41107  dvh0g  41110  djavalN  41134  diblsmopel  41170  dicvaddcl  41189  cdlemn6  41201  dihffval  41229  dihopelvalcpre  41247  djhval  41397  lcdvaddval  41597  lcdsmul  41601  lcdvsval  41603  lcdlkreq2N  41622  hvmapffval  41757  hvmapfval  41758  hdmap1fval  41795  hgmapffval  41884  hgmapfval  41885  hgmapadd  41893  hlhilipval  41948  hlhilhillem  41959  isprimroot  42086  aks6d1c1p4  42104  idomnnzpownz  42125  aks6d1c5lem1  42129  aks6d1c5lem3  42130  aks6d1c5lem2  42131  aks5lem3a  42182  unitscyglem5  42192  rhmpsr1  42546  selvvvval  42578  mhphf2  42591  prjspval  42596  prjspner1  42619  sn-isghm  42666  mnringvald  44206  ioorrnopnlem  46305  hoidmvval0b  46591  hoidmvlelem2  46597  hoidmvlelem3  46598  hoidmvle  46601  ovnhoi  46604  hoiqssbl  46626  hspmbllem2  46628  vonioo  46683  vonicc  46686  zlidlring  48238  uzlidlring  48239  ovmpordxf  48343  lincop  48413  lincval  48414  lincsum  48434  lincscm  48435  lmod1lem2  48493  lmod1lem3  48494  lmod1lem4  48495  ldepsnlinc  48513  lines  48736  line  48737  rrxlines  48738  rrxline  48739  spheres  48751  fvconstr  48866  fvconstrn0  48867  fvconstr2  48868  catprs  49016  sectrcl2  49028  invrcl2  49030  invfn  49035  isorcl2  49039  sectpropdlem  49041  invpropdlem  49043  isopropdlem  49045  cicpropdlem  49054  iinfconstbas  49071  nelsubclem  49072  nelsubc3lem  49075  ssccatid  49077  resccatlem  49078  cofu2a  49100  cofid2a  49118  cofid2  49120  cofidf2a  49122  cofidf2  49125  oppf2  49145  upfval  49181  upfval2  49182  upfval3  49183  upeu3  49200  upeu4  49201  oppcup3  49214  natoppfb  49236  swapfval  49267  swapf2a  49276  1stfpropd  49295  2ndfpropd  49296  cofuswapf2  49300  tposcurf12  49303  tposcurf2  49305  tposcurf2cl  49307  fucofvalg  49323  fuco11b  49342  fuco23a  49357  precofval3  49376  prcofpropd  49384  catcrcl2  49401  opf12  49409  fucoppcco  49414  thincmod  49435  isthincd2lem2  49440  isthincd  49441  dfinito4  49506  mndtcco2  49591  mndtccatid  49592  oppgoppchom  49595  oppgoppcco  49596  grptcmon  49598  grptcepi  49599  2arwcatlem2  49601  2arwcatlem3  49602  2arwcatlem4  49603  2arwcat  49605  lanrcl  49626  ranrcl  49627  rellan  49628  relran  49629  concom  49668  coccom  49669