Theorem oveqd 7428

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

Syntax hints:   → wi 4   = wceq 1567  (class class class)co 7411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3463  df-ss 3928  df-uni 4875  df-br 5112  df-iota 6493  df-fv 6545  df-ov 7414

This theorem is referenced by:  oveq123d  7432  oveqdr  7439  csbov  7456  csbov12g  7457  ovmpodxf  7561  oprssov  7580  2mpo0  7660  ofeqd  7677  mptmpoopabbrd  8078  mptmpoopabovd  8079  el2mpocsbcl  8080  fnmpoovd  8082  frecseq123  8279  ruclem1  16287  vdwapval  17033  vdwapid1  17035  vdwmc2  17039  vdwpc  17040  vdwlem5  17045  vdwlem8  17048  vdwlem13  17053  prdsval  17508  prdsdsval2  17537  pwsplusgval  17544  pwsmulrval  17545  pwsvscafval  17548  imasval  17565  iscat  17728  iscatd  17729  catidex  17730  catideu  17731  cidfval  17732  cidval  17733  catidd  17736  iscatd2  17737  catlid  17739  catrid  17740  homffval  17746  homfeqd  17751  homfeqval  17753  comfffval  17754  comffval  17755  comfeq  17762  comfeqd  17763  comfeqval  17764  catpropd  17765  oppcval  17769  oppcco  17773  monfval  17789  ismon  17790  oppcmon  17795  oppcepi  17796  sectffval  17807  sectfval  17808  invffval  17815  isoval  17822  dfiso2  17829  isofn  17832  invisoinvl  17847  invcoisoid  17849  isocoinvid  17850  issubc  17892  issubc3  17906  isfunc  17921  cofuval  17939  cofuval2  17944  funcres  17953  funcres2b  17954  funcres2  17955  idfusubc  17957  funcres2c  17960  isfull  17969  isfth  17973  fullres2c  17998  natfval  18006  isnat  18007  fucval  18018  fucco  18022  fucpropd  18037  initoval  18050  termoval  18051  homarcl  18085  coafval  18121  resssetc  18149  resscatc  18166  catciso  18168  xpcval  18233  1stfval  18247  2ndfval  18250  prfval  18255  prfcl  18259  evlfval  18273  curfval  18279  curf1cl  18284  curfcl  18288  uncf1  18292  uncf2  18293  diag12  18300  diag2  18301  curf2ndf  18303  hofval  18308  hof1  18310  hof2fval  18311  hofcl  18315  yon12  18321  yon2  18322  hofpropd  18323  joinval  18431  meetval  18445  isdlat  18578  plusffval  18704  ismgmd  18710  issstrmgm  18711  grpidval  18719  grpidd  18729  gsumvalx  18734  gsumpropd  18736  gsumress  18740  ismgmhm  18754  issubmgm  18760  resmgmhm  18769  resmgmhm2  18770  resmgmhm2b  18771  issgrpd  18788  ismndd  18814  issubmnd  18819  submnd0  18821  ismhm  18843  issubm  18861  resmhm  18879  resmhm2  18880  resmhm2b  18881  mhmimalem  18883  isgrp  19006  isgrpd2e  19022  grpidd2  19044  grpinvfval  19045  grpinvfvalALT  19046  imasgrp2  19121  imasgrp  19122  subg0  19198  subginv  19199  subgcl  19202  issubgrpd2  19209  isnsg  19221  isghm  19286  resghm  19302  isga  19361  subgga  19370  gasubg  19372  cntzfval  19390  resscntz  19403  odfval  19602  odfvalALT  19603  gexval  19648  lsmfval  19708  lsmvalx  19709  oppglsm  19712  subglsm  19743  pj1fval  19764  efgtval  19793  iscmn  19859  iscmnd  19864  submcmn2  19909  imasabl  19946  iscyg  19949  cycsubmcmn  19959  isomnd  20193  submomnd  20202  prdsmgp  20227  rngpropd  20252  ringurd  20267  issrg  20270  isring  20319  ringidss  20360  mulgass3  20435  dvdsrval  20443  rdivmuldivd  20495  isirred  20501  rnghmval  20522  islring  20625  lringuplu  20629  subrngmcl  20642  subrg1  20667  subrgdvds  20671  subrguss  20672  subrginv  20673  subrgdv  20674  subrgunit  20675  subrgugrp  20676  rnghmresel  20705  rngchom  20708  rngcco  20712  rnghmsubcsetclem1  20716  rhmresel  20734  ringchom  20737  ringcco  20741  rhmsubcsetclem1  20745  rhmsubcrngclem1  20751  rrgval  20782  isdrngd  20847  isdrngrd  20848  isdrngdOLD  20849  isdrngrdOLD  20850  abvfval  20891  isabvd  20893  issrngd  20936  isorng  20942  suborng  20957  islmod  20963  islmodd  20965  scaffval  20979  lmodpropd  21024  lssset  21032  islssd  21034  prdslmodd  21068  islmhm  21126  reslmhm  21151  reslmhm2  21152  reslmhm2b  21153  islbs  21175  rlmvneg  21305  rnglidlmmgm  21353  rnglidlmsgrp  21354  rnglidlrng  21355  lsmidllsp  21357  rngqiprngghmlem3  21400  rngqiprngimfolem  21401  rngqiprnglinlem1  21402  rngqiprngimf1  21411  rngqiprnglin  21413  rng2idl1cntr  21416  rngqiprngfulem5  21426  prmidlval  21433  irinitoringc  21598  isphl  21747  ipffval  21767  isphld  21773  phssipval  21776  phssip  21777  phlssphl  21778  ocvfval  21785  isobs  21839  frlmplusgval  21883  frlmsubgval  21884  frlmvscafval  21885  frlmip  21897  frlmipval  21898  frlmup1  21917  lsslindf  21949  isassa  21975  isassad  21984  sraassab  21987  assamulgscmlem2  22019  psrval  22034  resspsradd  22093  resspsrmul  22094  resspsrvsca  22095  mplmon2mul  22189  selvvvval  22262  ply1coe  22427  ply1chr  22435  lply1binomsc  22440  evl1expd  22474  evl1scvarpw  22492  asclply1subcl  22503  mamufval  22518  matplusg2  22553  matvsca2  22554  matplusgcell  22559  matsubgcell  22560  matinvgcell  22561  matvscacell  22562  matmulcell  22571  mpomatmul  22572  mat1  22573  mattposm  22585  mat1dimmul  22602  dmatmul  22623  dmatcrng  22628  scmataddcl  22642  scmatsubcl  22643  scmatcrng  22647  smatvscl  22650  scmatghm  22659  scmatmhm  22660  mvmulfval  22668  ma1repveval  22697  mdetrlin  22728  mdetrsca  22729  mdetmul  22749  madurid  22770  minmar1cl  22777  smadiadetglem1  22797  smadiadetr  22801  matinv  22803  slesolinv  22806  slesolinvbi  22807  cramerimplem3  22811  cpmatacl  22842  mat2pmatghm  22856  decpmatmullem  22897  decpmatmul  22898  pmatcollpw1lem1  22900  pmatcollpw2lem  22903  pmatcollpwlem  22906  pmatcollpw3lem  22909  mply1topmatval  22930  mp2pm2mplem1  22932  mp2pm2mplem4  22935  mp2pm2mplem5  22936  mp2pm2mp  22937  chpmat1d  22962  chpscmatgsummon  22971  chfacfpmmulgsum2  22991  xkocnv  23940  submtmd  24230  prdsdsf  24493  ressprdsds  24497  blfvalps  24509  prdsxmslem2  24655  tmsxpsval  24664  ngpds  24730  sgrimval  24758  subgngp  24761  tngngp  24780  tngngp3  24782  isnlm  24801  lssnlm  24827  isphtpy  25109  isphtpc  25122  pi1cpbl  25172  pi1addf  25175  pi1addval  25176  pi1grplem  25177  clmsub  25208  clmvsass  25217  clmvsdir  25219  isclmp  25225  cvsdiv  25260  iscph  25298  cphdir  25333  cphdi  25334  cph2di  25335  cph2subdi  25338  cphass  25339  tcphval  25346  ipcau2  25362  tcphcphlem1  25363  tcphcphlem2  25364  cphsscph  25379  caufval  25403  rrxip  25518  rrxvsca  25522  rrxplusgvscavalb  25523  rrxdsfival  25541  ehleudisval  25547  dvlip2  26123  q1pval  26281  r1pval  26284  dvntaylp  26500  efabl  26681  efsubm  26682  dchrmul  27378  seqseq123d  28445  istrkgc  28689  istrkgb  28690  istrkgcb  28691  istrkge  28692  istrkgl  28693  istrkgld  28694  iscgrg  28747  isismt  28769  tglngval  28786  legval  28819  ishlg  28837  mirval  28894  israg  28936  ishpg  29000  tgplnfn  29015  plngval  29017  isplng  29018  lmif  29052  islmib  29054  isinag  29110  ttgval  29165  wksonproplem  29993  wspthsnon  30142  iswwlksnon  30143  iswspthsnon  30146  isconngr  30481  isconngr1  30482  grpodivval  30828  dipfval  30995  ipval  30996  sspgval  31022  sspsval  31024  lnoval  31045  ajfval  31102  dipdir  31135  dipass  31138  htth  31211  ressmulgnn0d  33305  inftmrel  33441  isinftm  33442  isslmd  33463  elrgspnlem1  33503  erlval  33519  rlocval  33520  rlocaddval  33530  rlocmulval  33531  subrdom  33546  resv1r  33602  idlinsubrg  33683  idlsrgval  33738  idlsrg0g  33741  rprmval  33751  ressply1evls1  33800  vietalem  33914  drgextlsp  33929  fedgmullem1  33964  fedgmullem2  33965  fedgmul  33966  extdg1id  34001  fldextrspunlsplem  34008  fldextrspunlsp  34009  extdgfialglem1  34027  extdgfialglem2  34028  algextdeglem8  34059  smatlem  34132  submatminr1  34145  metidval  34225  pstmval  34230  pstmfval  34231  zlm0  34295  zlm1  34296  sitmval  34684  breprexp  34965  istrkg2d  34998  afsval  35006  mclsrcl  35986  mppsval  35997  bj-endval  37882  matunitlindflem2  38191  istotbnd  38343  isbnd  38354  rrnequiv  38409  isrngo  38471  rngohomval  38538  idlval  38587  pridlval  38607  lflset  39758  islfld  39761  ldualvadd  39828  ldualsmul  39834  ldualvs  39836  isopos  39879  cmtfvalN  39909  iscvlat  40022  ishlat1  40051  lineset  40437  psubspset  40443  paddfval  40496  paddval  40497  ltrnfset  40816  trnfsetN  40854  trlfset  40859  tgrpov  41447  erngplus  41502  erngmul  41505  erngplus-rN  41510  erngmul-rN  41513  erngdvlem3  41689  erngdvlem4  41690  erng0g  41693  erngdvlem3-rN  41697  erngdvlem4-rN  41698  dvaplusg  41708  dvamulr  41711  dvavadd  41714  dvavsca  41716  dvalveclem  41724  dvhmulr  41785  dvhfvadd  41790  dvhvadd  41791  dvhopvadd2  41793  dvhvaddcl  41794  dvhvaddcomN  41795  dvhvsca  41800  dvhlveclem  41807  dvh0g  41810  djavalN  41834  diblsmopel  41870  dicvaddcl  41889  cdlemn6  41901  dihffval  41929  dihopelvalcpre  41947  djhval  42097  lcdvaddval  42297  lcdsmul  42301  lcdvsval  42303  lcdlkreq2N  42322  hvmapffval  42457  hvmapfval  42458  hdmap1fval  42495  hgmapffval  42584  hgmapfval  42585  hgmapadd  42593  hlhilipval  42648  hlhilhillem  42659  isprimroot  42785  aks6d1c1p4  42803  idomnnzpownz  42824  aks6d1c5lem1  42828  aks6d1c5lem3  42829  aks6d1c5lem2  42830  aks5lem3a  42881  unitscyglem5  42891  rhmpsr1  43243  mhphf2  43257  prjspval  43262  prjspner1  43285  sn-isghm  43332  mnringvald  44864  ioorrnopnlem  46945  hoidmvval0b  47231  hoidmvlelem2  47237  hoidmvlelem3  47238  hoidmvle  47241  ovnhoi  47244  hoiqssbl  47266  hspmbllem2  47268  vonioo  47323  vonicc  47326  zlidlring  48923  uzlidlring  48924  ovmpordxf  49039  lincop  49108  lincval  49109  lincsum  49129  lincscm  49130  lmod1lem2  49188  lmod1lem3  49189  lmod1lem4  49190  ldepsnlinc  49208  lines  49431  line  49432  rrxlines  49433  rrxline  49434  spheres  49446  fvconstr  49560  fvconstrn0  49561  fvconstr2  49562  catprs  49709  sectrcl2  49721  invrcl2  49723  invfn  49728  isorcl2  49732  sectpropdlem  49734  invpropdlem  49736  isopropdlem  49738  cicpropdlem  49747  iinfconstbas  49764  nelsubclem  49765  nelsubc3lem  49768  ssccatid  49770  resccatlem  49771  cofu2a  49793  cofid2a  49811  cofid2  49813  cofidf2a  49815  cofidf2  49818  oppf2  49838  upfval  49874  upfval2  49875  upfval3  49876  upeu3  49893  upeu4  49894  oppcup3  49907  natoppfb  49929  swapfval  49960  swapf2a  49969  1stfpropd  49988  2ndfpropd  49989  cofuswapf2  49993  tposcurf12  49996  tposcurf2  49998  tposcurf2cl  50000  fucofvalg  50016  fuco11b  50035  fuco23a  50050  precofval3  50069  prcofpropd  50077  catcrcl2  50094  opf12  50102  fucoppcco  50107  thincmod  50128  isthincd2lem2  50133  isthincd  50134  dfinito4  50199  mndtcco2  50284  mndtccatid  50285  oppgoppchom  50288  oppgoppcco  50289  grptcmon  50291  grptcepi  50292  2arwcatlem2  50294  2arwcatlem3  50295  2arwcatlem4  50296  2arwcat  50298  lanrcl  50319  ranrcl  50320  rellan  50321  relran  50322  concom  50361  coccom  50362