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

Theorem adddid 9616
Description: Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1  |-  ( ph  ->  A  e.  CC )
addcld.2  |-  ( ph  ->  B  e.  CC )
addassd.3  |-  ( ph  ->  C  e.  CC )
Assertion
Ref Expression
adddid  |-  ( ph  ->  ( A  x.  ( B  +  C )
)  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )

Proof of Theorem adddid
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addcld.2 . 2  |-  ( ph  ->  B  e.  CC )
3 addassd.3 . 2  |-  ( ph  ->  C  e.  CC )
4 adddi 9577 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
51, 2, 3, 4syl3anc 1228 1  |-  ( ph  ->  ( A  x.  ( B  +  C )
)  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767  (class class class)co 6282   CCcc 9486    + caddc 9491    x. cmul 9493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 9555
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
This theorem is referenced by:  addid1  9755  cnegex  9756  addcom  9761  addcomd  9777  subdi  9986  conjmul  10257  cju  10528  flhalf  11926  modcyc  11995  binom3  12251  bcpasc  12363  hashf1lem2  12467  remim  12909  mulre  12913  readd  12918  remullem  12920  imadd  12926  cjadd  12933  sqreulem  13151  iseraltlem2  13464  o1fsum  13586  binomlem  13600  climcndslem2  13621  tanval3  13726  sinadd  13756  tanadd  13759  dvdsmulgcd  14047  pythagtriplem1  14195  pcaddlem  14262  prmreclem4  14292  prmreclem6  14294  mul4sqlem  14326  vdwlem3  14356  vdwlem6  14359  vdwlem9  14362  nn0srg  18254  rge0srg  18255  icopnfcnv  21177  pcoass  21259  minveclem2  21576  pjthlem1  21587  ovolunlem1a  21642  ovolscalem1  21659  itgcnlem  21931  itgadd  21966  itgmulc2  21975  itgsplit  21977  aaliou3lem2  22473  abelthlem7  22567  tangtx  22631  tanarg  22732  logcnlem4  22754  mulcxp  22794  cxpmul2  22798  heron  22897  quad2  22898  dcubic1lem  22902  dcubic2  22903  mcubic  22906  binom4  22909  quart1  22915  atanlogsublem  22974  2efiatan  22977  basellem2  23083  basellem3  23084  basellem8  23089  chtub  23215  bposlem9  23295  lgseisenlem2  23353  2sqlem4  23370  2sqlem8  23375  dchrisumlem1  23402  dchrvmasum2if  23410  dchrisum0re  23426  mulog2sumlem1  23447  selberglem1  23458  selberglem2  23459  selberg  23461  selberg2  23464  chpdifbndlem1  23466  selberg3lem1  23470  selberg4  23474  pntsval2  23489  pntibndlem2  23504  pntlemr  23515  pntlemf  23518  pntlemo  23520  ostth2lem2  23547  ostth2lem3  23548  brbtwn2  23884  axsegconlem9  23904  axpasch  23920  axeuclidlem  23941  axcontlem2  23944  axcontlem4  23946  axcontlem7  23949  axcontlem8  23950  ipasslem2  25423  minvecolem2  25467  pjhthlem1  25985  lgamgulmlem3  28213  subfacval2  28271  subfaclim  28272  binomfallfaclem2  28739  faclimlem1  28745  bpoly4  29398  itgaddnc  29652  itgmulc2nc  29660  dvasin  29680  pellexlem6  30374  pell1234qrmulcl  30395  rmxyadd  30461  jm2.25  30545  lcmgcdlem  30812  m1expeven  31141  sumnnodd  31172  stoweidlem13  31313  wallispilem4  31368  wallispi2lem1  31371  wallispi2lem2  31372  stirlinglem1  31374  stirlinglem6  31379  stirlinglem7  31380  stirlinglem8  31381  stirlinglem10  31383  dirkerper  31396  dirkertrigeqlem1  31398  dirkertrigeqlem2  31399  dirkertrigeqlem3  31400  fourierdlem83  31490  altgsumbcALT  32006
  Copyright terms: Public domain W3C validator