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

Theorem adddird 9407
Description: Distributive law (right-distributivity). (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 9373 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  x.  C )  =  ( ( A  x.  C )  +  ( B  x.  C
) ) )
51, 2, 3, 4syl3anc 1213 1  |-  ( ph  ->  ( ( A  +  B )  x.  C
)  =  ( ( A  x.  C )  +  ( B  x.  C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364    e. wcel 1761  (class class class)co 6090   CCcc 9276    + caddc 9281    x. cmul 9283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-addcl 9338  ax-mulcom 9342  ax-distr 9345
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-iota 5378  df-fv 5423  df-ov 6093
This theorem is referenced by:  1p1times  9536  recextlem1  9962  divdir  10013  2times  10436  ltdifltdiv  11674  modvalp1  11722  subsq  11969  subsq2  11970  binom3  11981  discr1  11996  cshweqrep  12451  remullem  12613  sqrlem7  12734  binomlem  13288  arisum  13318  smumullem  13684  bezoutlem3  13720  bezoutlem4  13721  pcexp  13922  mul4sqlem  14010  vdwapun  14031  mulgnnass  15648  cnfldmulg  17807  nn0srg  17840  rge0srg  17841  nmotri  20277  blcvx  20334  itg1addlem5  21137  mbfi1fseqlem4  21155  itgconst  21255  itgmulc2  21270  dvexp  21386  dvcvx  21451  plyaddlem1  21640  dgrcolem1  21699  abelthlem2  21856  abelthlem7  21862  tangtx  21926  cxpadd  22083  dcubic  22200  binom4  22204  dquartlem2  22206  dquart  22207  quart1lem  22209  quart1  22210  cvxcl  22337  scvxcvx  22338  basellem9  22385  bposlem9  22590  lgsquad2lem1  22656  2sqlem4  22665  2sqblem  22675  dchrisumlem2  22698  dchrisum0lem1  22724  mudivsum  22738  chpdifbndlem1  22761  pntrlog2bndlem2  22786  pntlemr  22810  pntlemk  22814  ostth2lem2  22842  brbtwn2  23086  ax5seglem3  23112  ax5seglem5  23114  axbtwnid  23120  axeuclidlem  23143  axcontlem2  23146  axcontlem4  23148  axcontlem7  23151  axcontlem8  23152  smcnlem  24027  subfacp1lem6  27003  subfacval2  27005  subfaclim  27006  cvxscon  27062  rescon  27065  binomfallfaclem2  27472  itg2addnclem3  28370  itgmulc2nc  28385  rrnequiv  28659  jm2.19lem3  29265  jm2.25  29273  jm3.1lem2  29292  itgsinexp  29720  stoweidlem11  29731  stoweidlem13  29733  stirlinglem1  29794  stirlinglem4  29797  sigaraf  29814  sineq0ALT  31507
  Copyright terms: Public domain W3C validator