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

Theorem adddird 8860
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 8830 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  x.  C )  =  ( ( A  x.  C )  +  ( B  x.  C
) ) )
51, 2, 3, 4syl3anc 1182 1  |-  ( ph  ->  ( ( A  +  B )  x.  C
)  =  ( ( A  x.  C )  +  ( B  x.  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684  (class class class)co 5858   CCcc 8735    + caddc 8740    x. cmul 8742
This theorem is referenced by:  1p1times  8983  recextlem1  9398  divdir  9447  2times  9843  subsq  11210  subsq2  11211  binom3  11222  discr1  11237  remullem  11613  sqrlem7  11734  binomlem  12287  arisum  12318  smumullem  12683  bezoutlem3  12719  bezoutlem4  12720  pcexp  12912  mul4sqlem  13000  vdwapun  13021  mulgnnass  14595  cnfldmulg  16406  nmotri  18248  blcvx  18304  itg1addlem5  19055  mbfi1fseqlem4  19073  itgconst  19173  itgmulc2  19188  dvexp  19302  dvcvx  19367  plyaddlem1  19595  dgrcolem1  19654  abelthlem2  19808  abelthlem7  19814  tangtx  19873  cxpadd  20026  dcubic  20142  binom4  20146  dquartlem2  20148  dquart  20149  quart1lem  20151  quart1  20152  cvxcl  20279  scvxcvx  20280  basellem9  20326  bposlem9  20531  lgsquad2lem1  20597  2sqlem4  20606  2sqblem  20616  dchrisumlem2  20639  dchrisum0lem1  20665  mudivsum  20679  chpdifbndlem1  20702  pntrlog2bndlem2  20727  pntlemr  20751  pntlemk  20755  ostth2lem2  20783  smcnlem  21270  subfacp1lem6  23716  subfacval2  23718  subfaclim  23719  cvxscon  23774  rescon  23777  brbtwn2  24533  ax5seglem3  24559  ax5seglem5  24561  axbtwnid  24567  axeuclidlem  24590  axcontlem2  24593  axcontlem4  24595  axcontlem7  24598  axcontlem8  24599  distsava  25689  rrnequiv  26559  jm2.19lem3  27084  jm2.25  27092  jm3.1lem2  27111  itgsinexp  27749  stirlinglem1  27823  stirlinglem4  27826  sigaraf  27843
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-addcl 8797  ax-mulcom 8801  ax-distr 8804
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861
  Copyright terms: Public domain W3C validator