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

Theorem adddid 9641
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 9602 . 2
51, 2, 3, 4syl3anc 1228 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  (class class class)co 6296   cc 9511   caddc 9516   cmul 9518
This theorem is referenced by:  addid1  9781  cnegex  9782  addcom  9787  addcomd  9803  subdi  10015  conjmul  10286  cju  10557  flhalf  11962  modcyc  12031  binom3  12287  bcpasc  12399  hashf1lem2  12505  remim  12950  mulre  12954  readd  12959  remullem  12961  imadd  12967  cjadd  12974  sqreulem  13192  iseraltlem2  13505  o1fsum  13627  binomlem  13641  climcndslem2  13662  tanval3  13869  sinadd  13899  tanadd  13902  dvdsmulgcd  14192  pythagtriplem1  14340  pcaddlem  14407  prmreclem4  14437  prmreclem6  14439  mul4sqlem  14471  vdwlem3  14501  vdwlem6  14504  vdwlem9  14507  nn0srg  18486  rge0srg  18487  icopnfcnv  21442  pcoass  21524  minveclem2  21841  pjthlem1  21852  ovolunlem1a  21907  ovolscalem1  21924  itgcnlem  22196  itgadd  22231  itgmulc2  22240  itgsplit  22242  aaliou3lem2  22739  abelthlem7  22833  tangtx  22898  efgh  22928  tanarg  23004  logcnlem4  23026  mulcxp  23066  cxpmul2  23070  heron  23169  quad2  23170  dcubic1lem  23174  dcubic2  23175  mcubic  23178  binom4  23181  quart1  23187  atanlogsublem  23246  2efiatan  23249  basellem2  23355  basellem3  23356  basellem8  23361  chtub  23487  bposlem9  23567  lgseisenlem2  23625  2sqlem4  23642  2sqlem8  23647  dchrisumlem1  23674  dchrvmasum2if  23682  dchrisum0re  23698  mulog2sumlem1  23719  selberglem1  23730  selberglem2  23731  selberg  23733  selberg2  23736  chpdifbndlem1  23738  selberg3lem1  23742  selberg4  23746  pntsval2  23761  pntibndlem2  23776  pntlemr  23787  pntlemf  23790  pntlemo  23792  ostth2lem2  23819  ostth2lem3  23820  brbtwn2  24208  axsegconlem9  24228  axpasch  24244  axeuclidlem  24265  axcontlem2  24268  axcontlem4  24270  axcontlem7  24273  axcontlem8  24274  ipasslem2  25747  minvecolem2  25791  pjhthlem1  26309  lgamgulmlem3  28573  subfacval2  28631  subfaclim  28632  binomfallfaclem2  29162  faclimlem1  29168  bpoly4  29821  itgaddnc  30075  itgmulc2nc  30083  dvasin  30103  pellexlem6  30770  pell1234qrmulcl  30791  rmxyadd  30857  jm2.25  30941  lcmgcdlem  31212  binomcxplemnotnn0  31261  m1expeven  31585  sumnnodd  31636  dvnmul  31740  stoweidlem13  31795  wallispilem4  31850  wallispi2lem1  31853  wallispi2lem2  31854  stirlinglem1  31856  stirlinglem6  31861  stirlinglem7  31862  stirlinglem8  31863  stirlinglem10  31865  dirkerper  31878  dirkertrigeqlem1  31880  dirkertrigeqlem2  31881  dirkertrigeqlem3  31882  fourierdlem83  31972  2zlidl  32740  2zrngamgm  32745  altgsumbcALT  32942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 9580
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator