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

Theorem adddird 9532
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 9498 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  x.  C )  =  ( ( A  x.  C )  +  ( B  x.  C
) ) )
51, 2, 3, 4syl3anc 1226 1  |-  ( ph  ->  ( ( A  +  B )  x.  C
)  =  ( ( A  x.  C )  +  ( B  x.  C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399    e. wcel 1826  (class class class)co 6196   CCcc 9401    + caddc 9406    x. cmul 9408
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-addcl 9463  ax-mulcom 9467  ax-distr 9470
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-iota 5460  df-fv 5504  df-ov 6199
This theorem is referenced by:  1p1times  9662  recextlem1  10096  divdir  10147  ltdifltdiv  11866  modvalp1  11915  subsq  12178  subsq2  12179  binom3  12189  discr1  12204  cshweqrep  12700  remullem  12963  sqrlem7  13084  binomlem  13643  arisum  13673  smumullem  14144  bezoutlem3  14180  bezoutlem4  14181  pcexp  14385  mul4sqlem  14473  vdwapun  14494  mulgnnass  16287  cnfldmulg  18563  nn0srg  18599  rge0srg  18600  nmotri  21331  blcvx  21388  itg1addlem5  22192  mbfi1fseqlem4  22210  itgconst  22310  itgmulc2  22325  dvexp  22441  dvcvx  22506  plyaddlem1  22695  dgrcolem1  22755  abelthlem2  22912  abelthlem7  22918  tangtx  22983  cxpadd  23147  dcubic  23293  binom4  23297  dquartlem2  23299  dquart  23300  quart1lem  23302  quart1  23303  cvxcl  23431  scvxcvx  23432  basellem9  23479  bposlem9  23684  lgsquad2lem1  23750  2sqlem4  23759  2sqblem  23769  dchrisumlem2  23792  dchrisum0lem1  23818  mudivsum  23832  chpdifbndlem1  23855  pntrlog2bndlem2  23880  pntlemr  23904  pntlemk  23908  ostth2lem2  23936  brbtwn2  24329  ax5seglem3  24355  ax5seglem5  24357  axbtwnid  24363  axeuclidlem  24386  axcontlem2  24389  axcontlem4  24391  axcontlem7  24394  axcontlem8  24395  ex-ind-dvds  25291  smcnlem  25724  subfacp1lem6  28818  subfacval2  28820  subfaclim  28821  cvxscon  28877  rescon  28880  binomfallfaclem2  29328  itg2addnclem3  30234  itgmulc2nc  30249  rrnequiv  30497  jm2.19lem3  31099  jm2.25  31107  jm3.1lem2  31126  binomcxplemwb  31421  binomcxplemnotnn0  31429  adddirp1d  31653  fperiodmullem  31669  coskpi2  31832  cosknegpi  31835  dvnmul  31906  stoweidlem11  31959  stoweidlem13  31961  stirlinglem1  32022  stirlinglem4  32025  dirkerper  32044  dirkertrigeqlem1  32046  dirkertrigeqlem2  32047  dirkertrigeqlem3  32048  dirkercncflem2  32052  fourierdlem41  32096  fourierdlem42  32097  fourierdlem64  32119  fourierswlem  32179  sigaraf  32236  joinlmuladdmuld  33521  sineq0ALT  34084  inductionexd  38496  int-leftdistd  38529  int-rightdistd  38530
  Copyright terms: Public domain W3C validator