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

Theorem adddii 9499
Description: Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.)
Hypotheses
Ref Expression
axi.1  |-  A  e.  CC
axi.2  |-  B  e.  CC
axi.3  |-  C  e.  CC
Assertion
Ref Expression
adddii  |-  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) )

Proof of Theorem adddii
StepHypRef Expression
1 axi.1 . 2  |-  A  e.  CC
2 axi.2 . 2  |-  B  e.  CC
3 axi.3 . 2  |-  C  e.  CC
4 adddi 9474 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
51, 2, 3, 4mp3an 1315 1  |-  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370    e. wcel 1758  (class class class)co 6192   CCcc 9383    + caddc 9388    x. cmul 9390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 9452
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  addid1  9652  3t3e9  10577  numltc  10878  numsucc  10884  numma  10889  4t3lem  10929  decbin2  10962  binom2i  12078  faclbnd4lem1  12172  mod2xnegi  14204  decsplit  14216  log2ublem1  22459  log2ublem2  22460  bposlem8  22748  ax5seglem7  23318  ip0i  24362  ip1ilem  24363  ipasslem10  24376  normlem0  24648  polid2i  24696  lnopunilem1  25551  2t6m3t4e0  30880
  Copyright terms: Public domain W3C validator