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

Theorem adddid 9104
Description: Distributive law. (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 9071 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
51, 2, 3, 4syl3anc 1184 1  |-  ( ph  ->  ( A  x.  ( B  +  C )
)  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725  (class class class)co 6073   CCcc 8980    + caddc 8985    x. cmul 8987
This theorem is referenced by:  addid1  9238  cnegex  9239  addcom  9244  addcomd  9260  subdi  9459  conjmul  9723  cju  9988  flhalf  11223  modcyc  11268  binom3  11492  bcpasc  11604  hashf1lem2  11697  remim  11914  mulre  11918  readd  11923  remullem  11925  imadd  11931  cjadd  11938  sqreulem  12155  iseraltlem2  12468  o1fsum  12584  binomlem  12600  climcndslem2  12622  tanval3  12727  sinadd  12757  tanadd  12760  dvdsmulgcd  13046  pythagtriplem1  13182  pcaddlem  13249  prmreclem4  13279  prmreclem6  13281  mul4sqlem  13313  vdwlem3  13343  vdwlem6  13346  vdwlem9  13349  icopnfcnv  18959  pcoass  19041  minveclem2  19319  pjthlem1  19330  ovolunlem1a  19384  ovolscalem1  19401  itgcnlem  19673  itgadd  19708  itgmulc2  19717  itgsplit  19719  aaliou3lem2  20252  abelthlem7  20346  tangtx  20405  tanarg  20506  logcnlem4  20528  mulcxp  20568  cxpmul2  20572  quad2  20671  dcubic1lem  20675  dcubic2  20676  mcubic  20679  binom4  20682  quart1  20688  atanlogsublem  20747  2efiatan  20750  basellem2  20856  basellem3  20857  basellem8  20862  chtub  20988  bposlem9  21068  lgseisenlem2  21126  2sqlem4  21143  2sqlem8  21148  dchrisumlem1  21175  dchrvmasum2if  21183  dchrisum0re  21199  mulog2sumlem1  21220  selberglem1  21231  selberglem2  21232  selberg  21234  selberg2  21237  chpdifbndlem1  21239  selberg3lem1  21243  selberg4  21247  pntsval2  21262  pntibndlem2  21277  pntlemr  21288  pntlemf  21291  pntlemo  21293  ostth2lem2  21320  ostth2lem3  21321  ipasslem2  22325  minvecolem2  22369  pjhthlem1  22885  lgamgulmlem3  24807  subfacval2  24865  subfaclim  24866  binomfallfaclem2  25348  faclimlem1  25354  brbtwn2  25836  axsegconlem9  25856  axpasch  25872  axeuclidlem  25893  axcontlem2  25896  axcontlem4  25898  axcontlem7  25901  axcontlem8  25902  bpoly4  26097  itgaddnc  26255  itgmulc2nc  26263  dvreasin  26280  pellexlem6  26888  pell1234qrmulcl  26909  rmxyadd  26975  jm2.25  27061  m1expeven  27692  stoweidlem13  27729  wallispilem4  27784  wallispi2lem1  27787  wallispi2lem2  27788  stirlinglem1  27790  stirlinglem6  27795  stirlinglem7  27796  stirlinglem8  27797  stirlinglem10  27799
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-distr 9049
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator