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

Theorem adddid 8859
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 8826 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
51, 2, 3, 4syl3anc 1182 1  |-  ( ph  ->  ( A  x.  ( B  +  C )
)  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684  (class class class)co 5858   CCcc 8735    + caddc 8740    x. cmul 8742
This theorem is referenced by:  addid1  8992  cnegex  8993  addcom  8998  addcomd  9014  subdi  9213  conjmul  9477  cju  9742  flhalf  10954  modcyc  10999  binom3  11222  bcpasc  11333  hashf1lem2  11394  remim  11602  mulre  11606  readd  11611  remullem  11613  imadd  11619  cjadd  11626  sqreulem  11843  iseraltlem2  12155  o1fsum  12271  binomlem  12287  climcndslem2  12309  tanval3  12414  sinadd  12444  tanadd  12447  dvdsmulgcd  12733  pythagtriplem1  12869  pcaddlem  12936  prmreclem4  12966  prmreclem6  12968  mul4sqlem  13000  vdwlem3  13030  vdwlem6  13033  vdwlem9  13036  icopnfcnv  18440  pcoass  18522  minveclem2  18790  pjthlem1  18801  ovolunlem1a  18855  ovolscalem1  18872  itgcnlem  19144  itgadd  19179  itgmulc2  19188  itgsplit  19190  aaliou3lem2  19723  abelthlem7  19814  tangtx  19873  tanarg  19970  logcnlem4  19992  mulcxp  20032  cxpmul2  20036  quad2  20135  dcubic1lem  20139  dcubic2  20140  mcubic  20143  binom4  20146  quart1  20152  atanlogsublem  20211  2efiatan  20214  basellem2  20319  basellem3  20320  basellem8  20325  chtub  20451  bposlem9  20531  lgseisenlem2  20589  2sqlem4  20606  2sqlem8  20611  dchrisumlem1  20638  dchrvmasum2if  20646  dchrisum0re  20662  mulog2sumlem1  20683  selberglem1  20694  selberglem2  20695  selberg  20697  selberg2  20700  chpdifbndlem1  20702  selberg3lem1  20706  selberg4  20710  pntsval2  20725  pntibndlem2  20740  pntlemr  20751  pntlemf  20754  pntlemo  20756  ostth2lem2  20783  ostth2lem3  20784  ipasslem2  21410  minvecolem2  21454  pjhthlem1  21970  subfacval2  23718  subfaclim  23719  brbtwn2  24533  axsegconlem9  24553  axpasch  24569  axeuclidlem  24590  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  axcontlem8  24599  bpoly4  24794  dvreasin  24923  mslb1  25607  pellexlem6  26919  pell1234qrmulcl  26940  rmxyadd  27006  jm2.25  27092  m1expeven  27725  wallispi2lem1  27820  wallispi2lem2  27821  stirlinglem1  27823  stirlinglem6  27828  stirlinglem7  27829  stirlinglem8  27830  stirlinglem10  27832
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-distr 8804
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator