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

Theorem adddird 9423
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 9389 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  x.  C )  =  ( ( A  x.  C )  +  ( B  x.  C
) ) )
51, 2, 3, 4syl3anc 1218 1  |-  ( ph  ->  ( ( A  +  B )  x.  C
)  =  ( ( A  x.  C )  +  ( B  x.  C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    e. wcel 1756  (class class class)co 6103   CCcc 9292    + caddc 9297    x. cmul 9299
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-addcl 9354  ax-mulcom 9358  ax-distr 9361
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rex 2733  df-rab 2736  df-v 2986  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896  df-uni 4104  df-br 4305  df-iota 5393  df-fv 5438  df-ov 6106
This theorem is referenced by:  1p1times  9552  recextlem1  9978  divdir  10029  2times  10452  ltdifltdiv  11690  modvalp1  11738  subsq  11985  subsq2  11986  binom3  11997  discr1  12012  cshweqrep  12467  remullem  12629  sqrlem7  12750  binomlem  13304  arisum  13334  smumullem  13700  bezoutlem3  13736  bezoutlem4  13737  pcexp  13938  mul4sqlem  14026  vdwapun  14047  mulgnnass  15667  cnfldmulg  17860  nn0srg  17893  rge0srg  17894  nmotri  20330  blcvx  20387  itg1addlem5  21190  mbfi1fseqlem4  21208  itgconst  21308  itgmulc2  21323  dvexp  21439  dvcvx  21504  plyaddlem1  21693  dgrcolem1  21752  abelthlem2  21909  abelthlem7  21915  tangtx  21979  cxpadd  22136  dcubic  22253  binom4  22257  dquartlem2  22259  dquart  22260  quart1lem  22262  quart1  22263  cvxcl  22390  scvxcvx  22391  basellem9  22438  bposlem9  22643  lgsquad2lem1  22709  2sqlem4  22718  2sqblem  22728  dchrisumlem2  22751  dchrisum0lem1  22777  mudivsum  22791  chpdifbndlem1  22814  pntrlog2bndlem2  22839  pntlemr  22863  pntlemk  22867  ostth2lem2  22895  brbtwn2  23163  ax5seglem3  23189  ax5seglem5  23191  axbtwnid  23197  axeuclidlem  23220  axcontlem2  23223  axcontlem4  23225  axcontlem7  23228  axcontlem8  23229  smcnlem  24104  subfacp1lem6  27085  subfacval2  27087  subfaclim  27088  cvxscon  27144  rescon  27147  binomfallfaclem2  27555  itg2addnclem3  28457  itgmulc2nc  28472  rrnequiv  28746  jm2.19lem3  29352  jm2.25  29360  jm3.1lem2  29379  itgsinexp  29807  stoweidlem11  29818  stoweidlem13  29820  stirlinglem1  29881  stirlinglem4  29884  sigaraf  29901  joinlmuladdmuld  31136  sineq0ALT  31685
  Copyright terms: Public domain W3C validator