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

Theorem adddird 9620
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 9586 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  x.  C )  =  ( ( A  x.  C )  +  ( B  x.  C
) ) )
51, 2, 3, 4syl3anc 1228 1  |-  ( ph  ->  ( ( A  +  B )  x.  C
)  =  ( ( A  x.  C )  +  ( B  x.  C ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767  (class class class)co 6283   CCcc 9489    + caddc 9494    x. cmul 9496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-addcl 9551  ax-mulcom 9555  ax-distr 9558
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5550  df-fv 5595  df-ov 6286
This theorem is referenced by:  1p1times  9749  recextlem1  10178  divdir  10229  2times  10653  ltdifltdiv  11933  modvalp1  11981  subsq  12242  subsq2  12243  binom3  12254  discr1  12269  cshweqrep  12751  remullem  12923  sqrlem7  13044  binomlem  13603  arisum  13633  smumullem  14000  bezoutlem3  14036  bezoutlem4  14037  pcexp  14241  mul4sqlem  14329  vdwapun  14350  mulgnnass  15977  cnfldmulg  18237  nn0srg  18270  rge0srg  18271  nmotri  20997  blcvx  21054  itg1addlem5  21858  mbfi1fseqlem4  21876  itgconst  21976  itgmulc2  21991  dvexp  22107  dvcvx  22172  plyaddlem1  22361  dgrcolem1  22420  abelthlem2  22577  abelthlem7  22583  tangtx  22647  cxpadd  22804  dcubic  22921  binom4  22925  dquartlem2  22927  dquart  22928  quart1lem  22930  quart1  22931  cvxcl  23058  scvxcvx  23059  basellem9  23106  bposlem9  23311  lgsquad2lem1  23377  2sqlem4  23386  2sqblem  23396  dchrisumlem2  23419  dchrisum0lem1  23445  mudivsum  23459  chpdifbndlem1  23482  pntrlog2bndlem2  23507  pntlemr  23531  pntlemk  23535  ostth2lem2  23563  brbtwn2  23900  ax5seglem3  23926  ax5seglem5  23928  axbtwnid  23934  axeuclidlem  23957  axcontlem2  23960  axcontlem4  23962  axcontlem7  23965  axcontlem8  23966  smcnlem  25299  subfacp1lem6  28285  subfacval2  28287  subfaclim  28288  cvxscon  28344  rescon  28347  binomfallfaclem2  28755  itg2addnclem3  29661  itgmulc2nc  29676  rrnequiv  29950  jm2.19lem3  30553  jm2.25  30561  jm3.1lem2  30580  adddirp1d  31079  fperiodmullem  31096  coskpi2  31218  cosknegpi  31221  itgsinexp  31288  stoweidlem11  31327  stoweidlem13  31329  stirlinglem1  31390  stirlinglem4  31393  dirkerper  31412  dirkertrigeqlem1  31414  dirkertrigeqlem2  31415  dirkertrigeqlem3  31416  dirkercncflem2  31420  fourierdlem41  31464  fourierdlem42  31465  fourierdlem64  31487  fourierswlem  31547  sigaraf  31553  joinlmuladdmuld  32277  sineq0ALT  32826
  Copyright terms: Public domain W3C validator