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

Theorem adddird 9069
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
adddird  |-  ( ph  ->  ( ( A  +  B )  x.  C
)  =  ( ( A  x.  C )  +  ( B  x.  C ) ) )

Proof of Theorem adddird
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 adddir 9039 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  x.  C )  =  ( ( A  x.  C )  +  ( B  x.  C
) ) )
51, 2, 3, 4syl3anc 1184 1  |-  ( ph  ->  ( ( A  +  B )  x.  C
)  =  ( ( A  x.  C )  +  ( B  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:  1p1times  9193  recextlem1  9608  divdir  9657  2times  10055  subsq  11443  subsq2  11444  binom3  11455  discr1  11470  remullem  11888  sqrlem7  12009  binomlem  12563  arisum  12594  smumullem  12959  bezoutlem3  12995  bezoutlem4  12996  pcexp  13188  mul4sqlem  13276  vdwapun  13297  mulgnnass  14873  cnfldmulg  16688  nmotri  18726  blcvx  18782  itg1addlem5  19545  mbfi1fseqlem4  19563  itgconst  19663  itgmulc2  19678  dvexp  19792  dvcvx  19857  plyaddlem1  20085  dgrcolem1  20144  abelthlem2  20301  abelthlem7  20307  tangtx  20366  cxpadd  20523  dcubic  20639  binom4  20643  dquartlem2  20645  dquart  20646  quart1lem  20648  quart1  20649  cvxcl  20776  scvxcvx  20777  basellem9  20824  bposlem9  21029  lgsquad2lem1  21095  2sqlem4  21104  2sqblem  21114  dchrisumlem2  21137  dchrisum0lem1  21163  mudivsum  21177  chpdifbndlem1  21200  pntrlog2bndlem2  21225  pntlemr  21249  pntlemk  21253  ostth2lem2  21281  smcnlem  22146  subfacp1lem6  24824  subfacval2  24826  subfaclim  24827  cvxscon  24883  rescon  24886  binomfallfaclem2  25307  brbtwn2  25748  ax5seglem3  25774  ax5seglem5  25776  axbtwnid  25782  axeuclidlem  25805  axcontlem2  25808  axcontlem4  25810  axcontlem7  25813  axcontlem8  25814  itg2addnclem3  26157  itgmulc2nc  26172  rrnequiv  26434  jm2.19lem3  26952  jm2.25  26960  jm3.1lem2  26979  itgsinexp  27616  stoweidlem11  27627  stoweidlem13  27629  stirlinglem1  27690  stirlinglem4  27693  sigaraf  27710
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-addcl 9006  ax-mulcom 9010  ax-distr 9013
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043
  Copyright terms: Public domain W3C validator