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

Theorem adddird 9113
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 9083 . 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 1652    e. wcel 1725  (class class class)co 6081   CCcc 8988    + caddc 8993    x. cmul 8995
This theorem is referenced by:  1p1times  9237  recextlem1  9652  divdir  9701  2times  10099  subsq  11488  subsq2  11489  binom3  11500  discr1  11515  remullem  11933  sqrlem7  12054  binomlem  12608  arisum  12639  smumullem  13004  bezoutlem3  13040  bezoutlem4  13041  pcexp  13233  mul4sqlem  13321  vdwapun  13342  mulgnnass  14918  cnfldmulg  16733  nmotri  18773  blcvx  18829  itg1addlem5  19592  mbfi1fseqlem4  19610  itgconst  19710  itgmulc2  19725  dvexp  19839  dvcvx  19904  plyaddlem1  20132  dgrcolem1  20191  abelthlem2  20348  abelthlem7  20354  tangtx  20413  cxpadd  20570  dcubic  20686  binom4  20690  dquartlem2  20692  dquart  20693  quart1lem  20695  quart1  20696  cvxcl  20823  scvxcvx  20824  basellem9  20871  bposlem9  21076  lgsquad2lem1  21142  2sqlem4  21151  2sqblem  21161  dchrisumlem2  21184  dchrisum0lem1  21210  mudivsum  21224  chpdifbndlem1  21247  pntrlog2bndlem2  21272  pntlemr  21296  pntlemk  21300  ostth2lem2  21328  smcnlem  22193  subfacp1lem6  24871  subfacval2  24873  subfaclim  24874  cvxscon  24930  rescon  24933  binomfallfaclem2  25356  brbtwn2  25844  ax5seglem3  25870  ax5seglem5  25872  axbtwnid  25878  axeuclidlem  25901  axcontlem2  25904  axcontlem4  25906  axcontlem7  25909  axcontlem8  25910  itg2addnclem3  26258  itgmulc2nc  26273  rrnequiv  26544  jm2.19lem3  27062  jm2.25  27070  jm3.1lem2  27089  itgsinexp  27725  stoweidlem11  27736  stoweidlem13  27738  stirlinglem1  27799  stirlinglem4  27802  sigaraf  27819  ltdifltdiv  28148  modvalp1  28151  cshweqrep  28274  sineq0ALT  29049
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-addcl 9050  ax-mulcom 9054  ax-distr 9057
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-rex 2711  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-iota 5418  df-fv 5462  df-ov 6084
  Copyright terms: Public domain W3C validator