MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  adddid Unicode version

Theorem adddid 9495
Description: Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1
addcld.2
addassd.3
Assertion
Ref Expression
adddid

Proof of Theorem adddid
StepHypRef Expression
1 addcld.1 . 2
2 addcld.2 . 2
3 addassd.3 . 2
4 adddi 9456 . 2
51, 2, 3, 4syl3anc 1219 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1370  e.wcel 1757  (class class class)co 6174   cc 9365   caddc 9370   cmul 9372
This theorem is referenced by:  addid1  9634  cnegex  9635  addcom  9640  addcomd  9656  subdi  9863  conjmul  10133  cju  10403  flhalf  11759  modcyc  11828  binom3  12070  bcpasc  12182  hashf1lem2  12295  remim  12692  mulre  12696  readd  12701  remullem  12703  imadd  12709  cjadd  12716  sqreulem  12933  iseraltlem2  13246  o1fsum  13362  binomlem  13378  climcndslem2  13399  tanval3  13504  sinadd  13534  tanadd  13537  dvdsmulgcd  13824  pythagtriplem1  13969  pcaddlem  14036  prmreclem4  14066  prmreclem6  14068  mul4sqlem  14100  vdwlem3  14130  vdwlem6  14133  vdwlem9  14136  nn0srg  17974  rge0srg  17975  icopnfcnv  20614  pcoass  20696  minveclem2  21013  pjthlem1  21024  ovolunlem1a  21079  ovolscalem1  21096  itgcnlem  21367  itgadd  21402  itgmulc2  21411  itgsplit  21413  aaliou3lem2  21909  abelthlem7  22003  tangtx  22067  tanarg  22168  logcnlem4  22190  mulcxp  22230  cxpmul2  22234  heron  22333  quad2  22334  dcubic1lem  22338  dcubic2  22339  mcubic  22342  binom4  22345  quart1  22351  atanlogsublem  22410  2efiatan  22413  basellem2  22519  basellem3  22520  basellem8  22525  chtub  22651  bposlem9  22731  lgseisenlem2  22789  2sqlem4  22806  2sqlem8  22811  dchrisumlem1  22838  dchrvmasum2if  22846  dchrisum0re  22862  mulog2sumlem1  22883  selberglem1  22894  selberglem2  22895  selberg  22897  selberg2  22900  chpdifbndlem1  22902  selberg3lem1  22906  selberg4  22910  pntsval2  22925  pntibndlem2  22940  pntlemr  22951  pntlemf  22954  pntlemo  22956  ostth2lem2  22983  ostth2lem3  22984  brbtwn2  23270  axsegconlem9  23290  axpasch  23306  axeuclidlem  23327  axcontlem2  23330  axcontlem4  23332  axcontlem7  23335  axcontlem8  23336  ipasslem2  24351  minvecolem2  24395  pjhthlem1  24913  lgamgulmlem3  27135  subfacval2  27193  subfaclim  27194  binomfallfaclem2  27661  faclimlem1  27667  bpoly4  28320  itgaddnc  28574  itgmulc2nc  28582  dvasin  28602  pellexlem6  29297  pell1234qrmulcl  29318  rmxyadd  29384  jm2.25  29470  m1expeven  29894  stoweidlem13  29930  wallispilem4  29985  wallispi2lem1  29988  wallispi2lem2  29989  stirlinglem1  29991  stirlinglem6  29996  stirlinglem7  29997  stirlinglem8  29998  stirlinglem10  30000  altgsumbcALT  30872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 9434
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
  Copyright terms: Public domain W3C validator