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

Theorem adddid 8875
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 8842 . 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 1632    e. wcel 1696  (class class class)co 5874   CCcc 8751    + caddc 8756    x. cmul 8758
This theorem is referenced by:  addid1  9008  cnegex  9009  addcom  9014  addcomd  9030  subdi  9229  conjmul  9493  cju  9758  flhalf  10970  modcyc  11015  binom3  11238  bcpasc  11349  hashf1lem2  11410  remim  11618  mulre  11622  readd  11627  remullem  11629  imadd  11635  cjadd  11642  sqreulem  11859  iseraltlem2  12171  o1fsum  12287  binomlem  12303  climcndslem2  12325  tanval3  12430  sinadd  12460  tanadd  12463  dvdsmulgcd  12749  pythagtriplem1  12885  pcaddlem  12952  prmreclem4  12982  prmreclem6  12984  mul4sqlem  13016  vdwlem3  13046  vdwlem6  13049  vdwlem9  13052  icopnfcnv  18456  pcoass  18538  minveclem2  18806  pjthlem1  18817  ovolunlem1a  18871  ovolscalem1  18888  itgcnlem  19160  itgadd  19195  itgmulc2  19204  itgsplit  19206  aaliou3lem2  19739  abelthlem7  19830  tangtx  19889  tanarg  19986  logcnlem4  20008  mulcxp  20048  cxpmul2  20052  quad2  20151  dcubic1lem  20155  dcubic2  20156  mcubic  20159  binom4  20162  quart1  20168  atanlogsublem  20227  2efiatan  20230  basellem2  20335  basellem3  20336  basellem8  20341  chtub  20467  bposlem9  20547  lgseisenlem2  20605  2sqlem4  20622  2sqlem8  20627  dchrisumlem1  20654  dchrvmasum2if  20662  dchrisum0re  20678  mulog2sumlem1  20699  selberglem1  20710  selberglem2  20711  selberg  20713  selberg2  20716  chpdifbndlem1  20718  selberg3lem1  20722  selberg4  20726  pntsval2  20741  pntibndlem2  20756  pntlemr  20767  pntlemf  20770  pntlemo  20772  ostth2lem2  20799  ostth2lem3  20800  ipasslem2  21426  minvecolem2  21470  pjhthlem1  21986  subfacval2  23733  subfaclim  23734  brbtwn2  24605  axsegconlem9  24625  axpasch  24641  axeuclidlem  24662  axcontlem2  24665  axcontlem4  24667  axcontlem7  24670  axcontlem8  24671  bpoly4  24866  itgaddnc  25011  itgmulc2nc  25019  dvreasin  25026  mslb1  25710  pellexlem6  27022  pell1234qrmulcl  27043  rmxyadd  27109  jm2.25  27195  m1expeven  27828  wallispi2lem1  27923  wallispi2lem2  27924  stirlinglem1  27926  stirlinglem6  27931  stirlinglem7  27932  stirlinglem8  27933  stirlinglem10  27935
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-distr 8820
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator