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

Theorem adddii 9638
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 9613 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
51, 2, 3, 4mp3an 1328 1  |-  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1407    e. wcel 1844  (class class class)co 6280   CCcc 9522    + caddc 9527    x. cmul 9529
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 9591
This theorem depends on definitions:  df-bi 187  df-an 371  df-3an 978
This theorem is referenced by:  addid1  9796  3t3e9  10731  numltc  11041  numsucc  11047  numma  11052  4t3lem  11092  decbin2  11125  binom2i  12324  faclbnd4lem1  12417  mod2xnegi  14768  decsplit  14780  log2ublem1  23604  log2ublem2  23605  bposlem8  23949  ax5seglem7  24667  ip0i  26167  ip1ilem  26168  ipasslem10  26181  normlem0  26453  polid2i  26501  lnopunilem1  27355  fourierswlem  37394  3exp4mod41  37875  2t6m3t4e0  38461
  Copyright terms: Public domain W3C validator