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

Theorem adddid 9068
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 9035 . 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 1649    e. wcel 1721  (class class class)co 6040   CCcc 8944    + caddc 8949    x. cmul 8951
This theorem is referenced by:  addid1  9202  cnegex  9203  addcom  9208  addcomd  9224  subdi  9423  conjmul  9687  cju  9952  flhalf  11186  modcyc  11231  binom3  11455  bcpasc  11567  hashf1lem2  11660  remim  11877  mulre  11881  readd  11886  remullem  11888  imadd  11894  cjadd  11901  sqreulem  12118  iseraltlem2  12431  o1fsum  12547  binomlem  12563  climcndslem2  12585  tanval3  12690  sinadd  12720  tanadd  12723  dvdsmulgcd  13009  pythagtriplem1  13145  pcaddlem  13212  prmreclem4  13242  prmreclem6  13244  mul4sqlem  13276  vdwlem3  13306  vdwlem6  13309  vdwlem9  13312  icopnfcnv  18920  pcoass  19002  minveclem2  19280  pjthlem1  19291  ovolunlem1a  19345  ovolscalem1  19362  itgcnlem  19634  itgadd  19669  itgmulc2  19678  itgsplit  19680  aaliou3lem2  20213  abelthlem7  20307  tangtx  20366  tanarg  20467  logcnlem4  20489  mulcxp  20529  cxpmul2  20533  quad2  20632  dcubic1lem  20636  dcubic2  20637  mcubic  20640  binom4  20643  quart1  20649  atanlogsublem  20708  2efiatan  20711  basellem2  20817  basellem3  20818  basellem8  20823  chtub  20949  bposlem9  21029  lgseisenlem2  21087  2sqlem4  21104  2sqlem8  21109  dchrisumlem1  21136  dchrvmasum2if  21144  dchrisum0re  21160  mulog2sumlem1  21181  selberglem1  21192  selberglem2  21193  selberg  21195  selberg2  21198  chpdifbndlem1  21200  selberg3lem1  21204  selberg4  21208  pntsval2  21223  pntibndlem2  21238  pntlemr  21249  pntlemf  21252  pntlemo  21254  ostth2lem2  21281  ostth2lem3  21282  ipasslem2  22286  minvecolem2  22330  pjhthlem1  22846  lgamgulmlem3  24768  subfacval2  24826  subfaclim  24827  binomfallfaclem2  25307  faclimlem1  25310  brbtwn2  25748  axsegconlem9  25768  axpasch  25784  axeuclidlem  25805  axcontlem2  25808  axcontlem4  25810  axcontlem7  25813  axcontlem8  25814  bpoly4  26009  itgaddnc  26164  itgmulc2nc  26172  dvreasin  26179  pellexlem6  26787  pell1234qrmulcl  26808  rmxyadd  26874  jm2.25  26960  m1expeven  27592  stoweidlem13  27629  wallispilem4  27684  wallispi2lem1  27687  wallispi2lem2  27688  stirlinglem1  27690  stirlinglem6  27695  stirlinglem7  27696  stirlinglem8  27697  stirlinglem10  27699
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-distr 9013
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator