Theorem oveqd 7429

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  (class class class)co 7412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-tru 1572  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7415

This theorem is used by:  oveq123d  7433  oveqdr  7440  csbov  7457  csbov12g  7458  ovmpodxf  7562  oprssov  7581  2mpo0  7661  ofeqd  7678  mptmpoopabbrd  8076  mptmpoopabovd  8077  el2mpocsbcl  8078  fnmpoovd  8080  frecseq123  8277  ruclem1  16293  vdwapval  17039  vdwapid1  17041  vdwmc2  17045  vdwpc  17046  vdwlem5  17051  vdwlem8  17054  vdwlem13  17059  prdsval  17514  prdsdsval2  17543  pwsplusgval  17550  pwsmulrval  17551  pwsvscafval  17554  imasval  17571  iscat  17734  iscatd  17735  catidex  17736  catideu  17737  cidfval  17738  cidval  17739  catidd  17742  iscatd2  17743  catlid  17745  catrid  17746  homffval  17752  homfeqd  17757  homfeqval  17759  comfffval  17760  comffval  17761  comfeq  17768  comfeqd  17769  comfeqval  17770  catpropd  17771  oppcval  17775  oppcco  17779  monfval  17795  ismon  17796  oppcmon  17801  oppcepi  17802  sectffval  17813  sectfval  17814  invffval  17821  isoval  17828  dfiso2  17835  isofn  17838  invisoinvl  17853  invcoisoid  17855  isocoinvid  17856  issubc  17898  issubc3  17912  isfunc  17927  cofuval  17945  cofuval2  17950  funcres  17959  funcres2b  17960  funcres2  17961  idfusubc  17963  funcres2c  17966  isfull  17975  isfth  17979  fullres2c  18004  natfval  18012  isnat  18013  fucval  18024  fucco  18028  fucpropd  18043  initoval  18056  termoval  18057  homarcl  18091  coafval  18127  resssetc  18155  resscatc  18172  catciso  18174  xpcval  18239  1stfval  18253  2ndfval  18256  prfval  18261  prfcl  18265  evlfval  18279  curfval  18285  curf1cl  18290  curfcl  18294  uncf1  18298  uncf2  18299  diag12  18306  diag2  18307  curf2ndf  18309  hofval  18314  hof1  18316  hof2fval  18317  hofcl  18321  yon12  18327  yon2  18328  hofpropd  18329  joinval  18437  meetval  18451  isdlat  18584  plusffval  18710  ismgmd  18716  issstrmgm  18717  grpidval  18725  grpidd  18735  gsumvalx  18740  gsumpropd  18742  gsumress  18746  ismgmhm  18760  issubmgm  18766  resmgmhm  18775  resmgmhm2  18776  resmgmhm2b  18777  issgrpd  18794  ismndd  18820  issubmnd  18825  submnd0  18827  ismhm  18849  issubm  18867  resmhm  18885  resmhm2  18886  resmhm2b  18887  mhmimalem  18889  isgrp  19012  isgrpd2e  19028  grpidd2  19050  grpinvfval  19051  grpinvfvalALT  19052  imasgrp2  19127  imasgrp  19128  subg0  19204  subginv  19205  subgcl  19208  issubgrpd2  19215  isnsg  19227  isghm  19292  resghm  19308  isga  19367  subgga  19376  gasubg  19378  cntzfval  19396  resscntz  19409  odfval  19608  odfvalALT  19609  gexval  19654  lsmfval  19714  lsmvalx  19715  oppglsm  19718  subglsm  19749  pj1fval  19770  efgtval  19799  iscmn  19865  iscmnd  19870  submcmn2  19915  imasabl  19952  iscyg  19955  cycsubmcmn  19965  isomnd  20199  submomnd  20208  prdsmgp  20233  rngpropd  20258  ringurd  20273  issrg  20276  isring  20325  ringidss  20367  mulgass3  20442  dvdsrval  20450  rdivmuldivd  20502  isirred  20508  rnghmval  20529  rhmval0  20564  islring  20650  lringuplu  20654  subrngmcl  20667  subrg1  20692  subrgdvds  20696  subrguss  20697  subrginv  20698  subrgdv  20699  subrgunit  20700  subrgugrp  20701  rnghmresel  20730  rngchom  20733  rngcco  20737  rnghmsubcsetclem1  20741  rhmresel  20759  ringchom  20762  ringcco  20766  rhmsubcsetclem1  20770  rhmsubcrngclem1  20776  rrgval  20807  isdrngd  20879  isdrngrd  20880  isdrngdOLD  20881  isdrngrdOLD  20882  abvfval  20924  isabvd  20926  issrngd  20969  isorng  20975  suborng  20990  islmod  20996  islmodd  20998  scaffval  21012  lmodpropd  21057  lssset  21065  islssd  21067  prdslmodd  21101  islmhm  21159  reslmhm  21184  reslmhm2  21185  reslmhm2b  21186  islbs  21208  rlmvneg  21338  rnglidlmmgm  21390  rnglidlmsgrp  21391  rnglidlrng  21392  lsmidllsp  21394  rngqiprngghmlem3  21440  rngqiprngimfolem  21441  rngqiprnglinlem1  21442  rngqiprngimf1  21451  rngqiprnglin  21453  rng2idl1cntr  21456  rngqiprngfulem5  21466  prmidlval  21473  irinitoringc  21640  isphl  21789  ipffval  21809  isphld  21815  phssipval  21818  phssip  21819  phlssphl  21820  ocvfval  21827  isobs  21881  frlmplusgval  21925  frlmsubgval  21926  frlmvscafval  21927  frlmip  21939  frlmipval  21940  frlmup1  21959  lsslindf  21991  isassa  22017  isassad  22026  sraassab  22029  assamulgscmlem2  22061  psrval  22076  resspsradd  22135  resspsrmul  22136  resspsrvsca  22137  mplmon2mul  22231  selvvvval  22304  ply1coe  22469  ply1chr  22477  lply1binomsc  22482  evl1expd  22516  evl1scvarpw  22534  asclply1subcl  22545  mamufval  22560  matplusg2  22595  matvsca2  22596  matplusgcell  22601  matsubgcell  22602  matinvgcell  22603  matvscacell  22604  matmulcell  22613  mpomatmul  22614  mat1  22615  mattposm  22627  mat1dimmul  22644  dmatmul  22665  dmatcrng  22670  scmataddcl  22684  scmatsubcl  22685  scmatcrng  22689  smatvscl  22692  scmatghm  22701  scmatmhm  22702  mvmulfval  22710  ma1repveval  22739  mdetrlin  22770  mdetrsca  22771  mdetmul  22791  madurid  22812  minmar1cl  22819  smadiadetglem1  22839  smadiadetr  22843  matinv  22845  slesolinv  22848  slesolinvbi  22849  cramerimplem3  22853  cpmatacl  22884  mat2pmatghm  22898  decpmatmullem  22939  decpmatmul  22940  pmatcollpw1lem1  22942  pmatcollpw2lem  22945  pmatcollpwlem  22948  pmatcollpw3lem  22951  mply1topmatval  22972  mp2pm2mplem1  22974  mp2pm2mplem4  22977  mp2pm2mplem5  22978  mp2pm2mp  22979  chpmat1d  23004  chpscmatgsummon  23013  chfacfpmmulgsum2  23033  xkocnv  23982  submtmd  24272  prdsdsf  24535  ressprdsds  24539  blfvalps  24551  prdsxmslem2  24697  tmsxpsval  24706  ngpds  24772  sgrimval  24800  subgngp  24803  tngngp  24822  tngngp3  24824  isnlm  24843  lssnlm  24869  isphtpy  25151  isphtpc  25164  pi1cpbl  25214  pi1addf  25217  pi1addval  25218  pi1grplem  25219  clmsub  25250  clmvsass  25259  clmvsdir  25261  isclmp  25267  cvsdiv  25302  iscph  25340  cphdir  25375  cphdi  25376  cph2di  25377  cph2subdi  25380  cphass  25381  tcphval  25388  ipcau2  25404  tcphcphlem1  25405  tcphcphlem2  25406  cphsscph  25421  caufval  25445  rrxip  25560  rrxvsca  25564  rrxplusgvscavalb  25565  rrxdsfival  25583  ehleudisval  25589  dvlip2  26165  q1pval  26323  r1pval  26326  dvntaylp  26545  efabl  26726  efsubm  26727  dchrmul  27423  seqseq123d  28490  istrkgc  28734  istrkgb  28735  istrkgcb  28736  istrkge  28737  istrkgl  28738  istrkgld  28739  iscgrg  28792  isismt  28814  tglngval  28831  legval  28864  ishlg2  28882  ishlg  28885  mirval  28943  israg  28988  ishpg  29052  tgplnfn  29068  plngval  29070  isplng  29071  lmif  29105  islmib  29107  isinag  29166  ttgval  29235  wksonproplem  30063  wspthsnon  30212  iswwlksnon  30213  iswspthsnon  30216  isconngr  30551  isconngr1  30552  grpodivval  30898  dipfval  31065  ipval  31066  sspgval  31092  sspsval  31094  lnoval  31115  ajfval  31172  dipdir  31205  dipass  31208  htth  31281  ressmulgnn0d  33373  inftmrel  33509  isinftm  33510  isslmd  33531  elrgspnlem1  33571  erlval  33587  rlocval  33588  rlocaddval  33598  rlocmulval  33599  subrdom  33614  resv1r  33668  idlinsubrg  33748  idlsrgval  33802  idlsrg0g  33805  rprmval  33815  ressply1evls1  33864  vietalem  33978  drgextlsp  33993  fedgmullem1  34028  fedgmullem2  34029  fedgmul  34030  extdg1id  34065  fldextrspunlsplem  34072  fldextrspunlsp  34073  extdgfialglem1  34091  extdgfialglem2  34092  algextdeglem8  34123  smatlem  34196  submatminr1  34209  metidval  34289  pstmval  34294  pstmfval  34295  zlm0  34359  zlm1  34360  sitmval  34748  breprexp  35029  istrkg2d  35062  afsval  35070  mclsrcl  36061  mppsval  36072  bj-endval  37987  matunitlindflem2  38296  istotbnd  38448  isbnd  38459  rrnequiv  38514  isrngo  38576  rngohomval  38643  idlval  38692  pridlval  38712  lflset  39861  islfld  39864  ldualvadd  39931  ldualsmul  39937  ldualvs  39939  isopos  39982  cmtfvalN  40012  iscvlat  40125  ishlat1  40154  lineset  40540  psubspset  40546  paddfval  40599  paddval  40600  ltrnfset  40919  trnfsetN  40957  trlfset  40962  tgrpov  41550  erngplus  41605  erngmul  41608  erngplus-rN  41613  erngmul-rN  41616  erngdvlem3  41792  erngdvlem4  41793  erng0g  41796  erngdvlem3-rN  41800  erngdvlem4-rN  41801  dvaplusg  41811  dvamulr  41814  dvavadd  41817  dvavsca  41819  dvalveclem  41827  dvhmulr  41888  dvhfvadd  41893  dvhvadd  41894  dvhopvadd2  41896  dvhvaddcl  41897  dvhvaddcomN  41898  dvhvsca  41903  dvhlveclem  41910  dvh0g  41913  djavalN  41937  diblsmopel  41973  dicvaddcl  41992  cdlemn6  42004  dihffval  42032  dihopelvalcpre  42050  djhval  42200  lcdvaddval  42400  lcdsmul  42404  lcdvsval  42406  lcdlkreq2N  42425  hvmapffval  42560  hvmapfval  42561  hdmap1fval  42598  hgmapffval  42687  hgmapfval  42688  hgmapadd  42696  hlhilipval  42751  hlhilhillem  42762  isprimroot  42888  aks6d1c1p4  42906  idomnnzpownz  42927  aks6d1c5lem1  42931  aks6d1c5lem3  42932  aks6d1c5lem2  42933  aks5lem3a  42984  unitscyglem5  42994  rhmpsr1  43344  mhphf2  43358  prjspval  43363  prjspner1  43386  sn-isghm  43433  mnringvald  44965  ioorrnopnlem  47046  hoidmvval0b  47332  hoidmvlelem2  47338  hoidmvlelem3  47339  hoidmvle  47342  ovnhoi  47345  hoiqssbl  47367  hspmbllem2  47369  vonioo  47424  vonicc  47427  zlidlring  49027  uzlidlring  49028  ovmpordxf  49147  lincop  49216  lincval  49217  lincsum  49237  lincscm  49238  lmod1lem2  49296  lmod1lem3  49297  lmod1lem4  49298  ldepsnlinc  49316  lines  49539  line  49540  rrxlines  49541  rrxline  49542  spheres  49554  fvconstr  49668  fvconstrn0  49669  fvconstr2  49670  catprs  49817  sectrcl2  49829  invrcl2  49831  invfn  49836  isorcl2  49840  sectpropdlem  49842  invpropdlem  49844  isopropdlem  49846  cicpropdlem  49855  iinfconstbas  49872  nelsubclem  49873  nelsubc3lem  49876  ssccatid  49878  resccatlem  49879  cofu2a  49901  cofid2a  49919  cofid2  49921  cofidf2a  49923  cofidf2  49926  oppf2  49946  upfval  49982  upfval2  49983  upfval3  49984  upeu3  50001  upeu4  50002  oppcup3  50015  natoppfb  50037  swapfval  50068  swapf2a  50077  1stfpropd  50096  2ndfpropd  50097  cofuswapf2  50101  tposcurf12  50104  tposcurf2  50106  tposcurf2cl  50108  fucofvalg  50124  fuco11b  50143  fuco23a  50158  precofval3  50177  prcofpropd  50185  catcrcl2  50202  opf12  50210  fucoppcco  50215  thincmod  50236  isthincd2lem2  50241  isthincd  50242  dfinito4  50307  mndtcco2  50392  mndtccatid  50393  oppgoppchom  50396  oppgoppcco  50397  grptcmon  50399  grptcepi  50400  2arwcatlem2  50402  2arwcatlem3  50403  2arwcatlem4  50404  2arwcat  50406  lanrcl  50427  ranrcl  50428  rellan  50429  relran  50430  concom  50469  coccom  50470