Theorem oveqd 7377

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

Syntax hints:   → wi 4   = wceq 1548  (class class class)co 7360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-v 3435  df-ss 3902  df-uni 4842  df-br 5076  df-iota 6445  df-fv 6497  df-ov 7363

This theorem is referenced by:  oveq123d  7381  oveqdr  7388  csbov  7405  csbov12g  7406  ovmpodxf  7510  oprssov  7529  2mpo0  7609  ofeqd  7626  mptmpoopabbrd  8026  mptmpoopabovd  8027  el2mpocsbcl  8028  fnmpoovd  8030  frecseq123  8226  ruclem1  16193  vdwapval  16939  vdwapid1  16941  vdwmc2  16945  vdwpc  16946  vdwlem5  16951  vdwlem8  16954  vdwlem13  16959  prdsval  17413  prdsdsval2  17442  pwsplusgval  17449  pwsmulrval  17450  pwsvscafval  17453  imasval  17470  iscat  17633  iscatd  17634  catidex  17635  catideu  17636  cidfval  17637  cidval  17638  catidd  17641  iscatd2  17642  catlid  17644  catrid  17645  homffval  17651  homfeqd  17656  homfeqval  17658  comfffval  17659  comffval  17660  comfeq  17667  comfeqd  17668  comfeqval  17669  catpropd  17670  oppcval  17674  oppcco  17678  monfval  17694  ismon  17695  oppcmon  17700  oppcepi  17701  sectffval  17712  sectfval  17713  invffval  17720  isoval  17727  dfiso2  17734  isofn  17737  invisoinvl  17752  invcoisoid  17754  isocoinvid  17755  issubc  17797  issubc3  17811  isfunc  17826  cofuval  17844  cofuval2  17849  funcres  17858  funcres2b  17859  funcres2  17860  idfusubc  17862  funcres2c  17865  isfull  17874  isfth  17878  fullres2c  17903  natfval  17911  isnat  17912  fucval  17923  fucco  17927  fucpropd  17942  initoval  17955  termoval  17956  homarcl  17990  coafval  18026  resssetc  18054  resscatc  18071  catciso  18073  xpcval  18138  1stfval  18152  2ndfval  18155  prfval  18160  prfcl  18164  evlfval  18178  curfval  18184  curf1cl  18189  curfcl  18193  uncf1  18197  uncf2  18198  diag12  18205  diag2  18206  curf2ndf  18208  hofval  18213  hof1  18215  hof2fval  18216  hofcl  18220  yon12  18226  yon2  18227  hofpropd  18228  joinval  18336  meetval  18350  isdlat  18483  plusffval  18609  ismgmd  18615  issstrmgm  18616  grpidval  18624  grpidd  18634  gsumvalx  18639  gsumpropd  18641  gsumress  18645  ismgmhm  18659  issubmgm  18665  resmgmhm  18674  resmgmhm2  18675  resmgmhm2b  18676  issgrpd  18693  ismndd  18719  issubmnd  18724  submnd0  18726  ismhm  18748  issubm  18766  resmhm  18783  resmhm2  18784  resmhm2b  18785  mhmimalem  18787  isgrp  18910  isgrpd2e  18926  grpidd2  18948  grpinvfval  18949  grpinvfvalALT  18950  imasgrp2  19026  imasgrp  19027  subg0  19103  subginv  19104  subgcl  19107  issubgrpd2  19113  isnsg  19125  isghm  19185  isghmOLD  19186  resghm  19202  isga  19261  subgga  19270  gasubg  19272  cntzfval  19290  resscntz  19303  odfval  19502  odfvalALT  19503  gexval  19548  lsmfval  19608  lsmvalx  19609  oppglsm  19612  subglsm  19643  pj1fval  19664  efgtval  19693  iscmn  19759  iscmnd  19764  submcmn2  19809  imasabl  19846  iscyg  19849  cycsubmcmn  19859  isomnd  20093  submomnd  20102  prdsmgp  20127  rngpropd  20150  ringurd  20161  issrg  20164  isring  20213  ringidss  20253  mulgass3  20328  dvdsrval  20336  rdivmuldivd  20388  isirred  20394  rnghmval  20415  islring  20516  lringuplu  20520  subrngmcl  20533  subrg1  20558  subrgdvds  20562  subrguss  20563  subrginv  20564  subrgdv  20565  subrgunit  20566  subrgugrp  20567  rnghmresel  20596  rngchom  20599  rngcco  20603  rnghmsubcsetclem1  20607  rhmresel  20625  ringchom  20628  ringcco  20632  rhmsubcsetclem1  20636  rhmsubcrngclem1  20642  rrgval  20673  isdrngd  20741  isdrngrd  20742  isdrngdOLD  20743  isdrngrdOLD  20744  abvfval  20786  isabvd  20788  issrngd  20831  isorng  20837  suborng  20852  islmod  20858  islmodd  20860  scaffval  20874  lmodpropd  20919  lssset  20927  islssd  20929  prdslmodd  20963  islmhm  21021  reslmhm  21046  reslmhm2  21047  reslmhm2b  21048  islbs  21070  rlmvneg  21200  rnglidlmmgm  21242  rnglidlmsgrp  21243  rnglidlrng  21244  rngqiprngghmlem3  21286  rngqiprngimfolem  21287  rngqiprnglinlem1  21288  rngqiprngimf1  21297  rngqiprnglin  21299  rng2idl1cntr  21302  rngqiprngfulem5  21312  irinitoringc  21458  isphl  21607  ipffval  21627  isphld  21633  phssipval  21636  phssip  21637  phlssphl  21638  ocvfval  21645  isobs  21699  frlmplusgval  21743  frlmsubgval  21744  frlmvscafval  21745  frlmip  21757  frlmipval  21758  frlmup1  21777  lsslindf  21809  isassa  21835  isassad  21844  sraassab  21847  assamulgscmlem2  21879  psrval  21894  resspsradd  21953  resspsrmul  21954  resspsrvsca  21955  mplmon2mul  22049  selvvvval  22122  ply1coe  22288  ply1chr  22296  lply1binomsc  22301  evl1expd  22335  evl1scvarpw  22353  asclply1subcl  22364  mamufval  22379  matplusg2  22414  matvsca2  22415  matplusgcell  22420  matsubgcell  22421  matinvgcell  22422  matvscacell  22423  matmulcell  22432  mpomatmul  22433  mat1  22434  mattposm  22446  mat1dimmul  22463  dmatmul  22484  dmatcrng  22489  scmataddcl  22503  scmatsubcl  22504  scmatcrng  22508  smatvscl  22511  scmatghm  22520  scmatmhm  22521  mvmulfval  22529  ma1repveval  22558  mdetrlin  22589  mdetrsca  22590  mdetmul  22610  madurid  22631  minmar1cl  22638  smadiadetglem1  22658  smadiadetr  22662  matinv  22664  slesolinv  22667  slesolinvbi  22668  cramerimplem3  22672  cpmatacl  22703  mat2pmatghm  22717  decpmatmullem  22758  decpmatmul  22759  pmatcollpw1lem1  22761  pmatcollpw2lem  22764  pmatcollpwlem  22767  pmatcollpw3lem  22770  mply1topmatval  22791  mp2pm2mplem1  22793  mp2pm2mplem4  22796  mp2pm2mplem5  22797  mp2pm2mp  22798  chpmat1d  22823  chpscmatgsummon  22832  chfacfpmmulgsum2  22852  xkocnv  23801  submtmd  24091  prdsdsf  24354  ressprdsds  24358  blfvalps  24370  prdsxmslem2  24516  tmsxpsval  24525  ngpds  24591  sgrimval  24619  subgngp  24622  tngngp  24641  tngngp3  24643  isnlm  24662  lssnlm  24688  isphtpy  24970  isphtpc  24983  pi1cpbl  25033  pi1addf  25036  pi1addval  25037  pi1grplem  25038  clmsub  25069  clmvsass  25078  clmvsdir  25080  isclmp  25086  cvsdiv  25121  iscph  25159  cphdir  25194  cphdi  25195  cph2di  25196  cph2subdi  25199  cphass  25200  tcphval  25207  ipcau2  25223  tcphcphlem1  25224  tcphcphlem2  25225  cphsscph  25240  caufval  25264  rrxip  25379  rrxvsca  25383  rrxplusgvscavalb  25384  rrxdsfival  25402  ehleudisval  25408  dvlip2  25984  q1pval  26142  r1pval  26145  dvntaylp  26358  efabl  26536  efsubm  26537  dchrmul  27233  seqseq123d  28300  istrkgc  28544  istrkgb  28545  istrkgcb  28546  istrkge  28547  istrkgl  28548  istrkgld  28549  iscgrg  28602  isismt  28624  tglngval  28641  legval  28674  ishlg  28692  mirval  28745  israg  28787  ishpg  28849  lmif  28875  islmib  28877  isinag  28928  ttgval  28965  wksonproplem  29793  wspthsnon  29942  iswwlksnon  29943  iswspthsnon  29946  isconngr  30281  isconngr1  30282  grpodivval  30628  dipfval  30795  ipval  30796  sspgval  30822  sspsval  30824  lnoval  30845  ajfval  30902  dipdir  30935  dipass  30938  htth  31011  ressmulgnn0d  33129  inftmrel  33265  isinftm  33266  isslmd  33287  elrgspnlem1  33327  erlval  33343  rlocval  33344  rlocaddval  33353  rlocmulval  33354  subrdom  33370  resv1r  33426  lsmidllsp  33487  idlinsubrg  33518  prmidlval  33524  idlsrgval  33598  idlsrg0g  33601  rprmval  33611  ressply1evls1  33660  vietalem  33775  drgextlsp  33790  fedgmullem1  33825  fedgmullem2  33826  fedgmul  33827  extdg1id  33862  fldextrspunlsplem  33869  fldextrspunlsp  33870  extdgfialglem1  33888  extdgfialglem2  33889  algextdeglem8  33920  smatlem  33993  submatminr1  34006  metidval  34086  pstmval  34091  pstmfval  34092  zlm0  34156  zlm1  34157  sitmval  34545  breprexp  34829  istrkg2d  34862  afsval  34870  mclsrcl  35804  mppsval  35815  bj-endval  37690  matunitlindflem2  37999  istotbnd  38151  isbnd  38162  rrnequiv  38217  isrngo  38279  rngohomval  38346  idlval  38395  pridlval  38415  lflset  39566  islfld  39569  ldualvadd  39636  ldualsmul  39642  ldualvs  39644  isopos  39687  cmtfvalN  39717  iscvlat  39830  ishlat1  39859  lineset  40245  psubspset  40251  paddfval  40304  paddval  40305  ltrnfset  40624  trnfsetN  40662  trlfset  40667  tgrpov  41255  erngplus  41310  erngmul  41313  erngplus-rN  41318  erngmul-rN  41321  erngdvlem3  41497  erngdvlem4  41498  erng0g  41501  erngdvlem3-rN  41505  erngdvlem4-rN  41506  dvaplusg  41516  dvamulr  41519  dvavadd  41522  dvavsca  41524  dvalveclem  41532  dvhmulr  41593  dvhfvadd  41598  dvhvadd  41599  dvhopvadd2  41601  dvhvaddcl  41602  dvhvaddcomN  41603  dvhvsca  41608  dvhlveclem  41615  dvh0g  41618  djavalN  41642  diblsmopel  41678  dicvaddcl  41697  cdlemn6  41709  dihffval  41737  dihopelvalcpre  41755  djhval  41905  lcdvaddval  42105  lcdsmul  42109  lcdvsval  42111  lcdlkreq2N  42130  hvmapffval  42265  hvmapfval  42266  hdmap1fval  42303  hgmapffval  42392  hgmapfval  42393  hgmapadd  42401  hlhilipval  42456  hlhilhillem  42467  isprimroot  42593  aks6d1c1p4  42611  idomnnzpownz  42632  aks6d1c5lem1  42636  aks6d1c5lem3  42637  aks6d1c5lem2  42638  aks5lem3a  42689  unitscyglem5  42699  rhmpsr1  43049  mhphf2  43063  prjspval  43068  prjspner1  43091  sn-isghm  43138  mnringvald  44672  ioorrnopnlem  46761  hoidmvval0b  47047  hoidmvlelem2  47053  hoidmvlelem3  47054  hoidmvle  47057  ovnhoi  47060  hoiqssbl  47082  hspmbllem2  47084  vonioo  47139  vonicc  47142  zlidlring  48739  uzlidlring  48740  ovmpordxf  48844  lincop  48913  lincval  48914  lincsum  48934  lincscm  48935  lmod1lem2  48993  lmod1lem3  48994  lmod1lem4  48995  ldepsnlinc  49013  lines  49236  line  49237  rrxlines  49238  rrxline  49239  spheres  49251  fvconstr  49366  fvconstrn0  49367  fvconstr2  49368  catprs  49515  sectrcl2  49527  invrcl2  49529  invfn  49534  isorcl2  49538  sectpropdlem  49540  invpropdlem  49542  isopropdlem  49544  cicpropdlem  49553  iinfconstbas  49570  nelsubclem  49571  nelsubc3lem  49574  ssccatid  49576  resccatlem  49577  cofu2a  49599  cofid2a  49617  cofid2  49619  cofidf2a  49621  cofidf2  49624  oppf2  49644  upfval  49680  upfval2  49681  upfval3  49682  upeu3  49699  upeu4  49700  oppcup3  49713  natoppfb  49735  swapfval  49766  swapf2a  49775  1stfpropd  49794  2ndfpropd  49795  cofuswapf2  49799  tposcurf12  49802  tposcurf2  49804  tposcurf2cl  49806  fucofvalg  49822  fuco11b  49841  fuco23a  49856  precofval3  49875  prcofpropd  49883  catcrcl2  49900  opf12  49908  fucoppcco  49913  thincmod  49934  isthincd2lem2  49939  isthincd  49940  dfinito4  50005  mndtcco2  50090  mndtccatid  50091  oppgoppchom  50094  oppgoppcco  50095  grptcmon  50097  grptcepi  50098  2arwcatlem2  50100  2arwcatlem3  50101  2arwcatlem4  50102  2arwcat  50104  lanrcl  50125  ranrcl  50126  rellan  50127  relran  50128  concom  50167  coccom  50168