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

Theorem adddid 9038
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 9005 . 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 1717  (class class class)co 6013   CCcc 8914    + caddc 8919    x. cmul 8921
This theorem is referenced by:  addid1  9171  cnegex  9172  addcom  9177  addcomd  9193  subdi  9392  conjmul  9656  cju  9921  flhalf  11151  modcyc  11196  binom3  11420  bcpasc  11532  hashf1lem2  11625  remim  11842  mulre  11846  readd  11851  remullem  11853  imadd  11859  cjadd  11866  sqreulem  12083  iseraltlem2  12396  o1fsum  12512  binomlem  12528  climcndslem2  12550  tanval3  12655  sinadd  12685  tanadd  12688  dvdsmulgcd  12974  pythagtriplem1  13110  pcaddlem  13177  prmreclem4  13207  prmreclem6  13209  mul4sqlem  13241  vdwlem3  13271  vdwlem6  13274  vdwlem9  13277  icopnfcnv  18831  pcoass  18913  minveclem2  19187  pjthlem1  19198  ovolunlem1a  19252  ovolscalem1  19269  itgcnlem  19541  itgadd  19576  itgmulc2  19585  itgsplit  19587  aaliou3lem2  20120  abelthlem7  20214  tangtx  20273  tanarg  20374  logcnlem4  20396  mulcxp  20436  cxpmul2  20440  quad2  20539  dcubic1lem  20543  dcubic2  20544  mcubic  20547  binom4  20550  quart1  20556  atanlogsublem  20615  2efiatan  20618  basellem2  20724  basellem3  20725  basellem8  20730  chtub  20856  bposlem9  20936  lgseisenlem2  20994  2sqlem4  21011  2sqlem8  21016  dchrisumlem1  21043  dchrvmasum2if  21051  dchrisum0re  21067  mulog2sumlem1  21088  selberglem1  21099  selberglem2  21100  selberg  21102  selberg2  21105  chpdifbndlem1  21107  selberg3lem1  21111  selberg4  21115  pntsval2  21130  pntibndlem2  21145  pntlemr  21156  pntlemf  21159  pntlemo  21161  ostth2lem2  21188  ostth2lem3  21189  ipasslem2  22174  minvecolem2  22218  pjhthlem1  22734  lgamgulmlem3  24587  subfacval2  24645  subfaclim  24646  faclimlem1  25113  brbtwn2  25551  axsegconlem9  25571  axpasch  25587  axeuclidlem  25608  axcontlem2  25611  axcontlem4  25613  axcontlem7  25616  axcontlem8  25617  bpoly4  25812  itgaddnc  25958  itgmulc2nc  25966  dvreasin  25973  pellexlem6  26581  pell1234qrmulcl  26602  rmxyadd  26668  jm2.25  26754  m1expeven  27386  stoweidlem13  27423  wallispilem4  27478  wallispi2lem1  27481  wallispi2lem2  27482  stirlinglem1  27484  stirlinglem6  27489  stirlinglem7  27490  stirlinglem8  27491  stirlinglem10  27493
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-distr 8983
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator