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

Theorem adddii 9383
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 9358 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
51, 2, 3, 4mp3an 1307 1  |-  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1362    e. wcel 1755  (class class class)co 6080   CCcc 9267    + caddc 9272    x. cmul 9274
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 9336
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 960
This theorem is referenced by:  addid1  9536  3t3e9  10461  numltc  10762  numsucc  10768  numma  10773  4t3lem  10813  decbin2  10846  binom2i  11958  faclbnd4lem1  12052  mod2xnegi  14082  decsplit  14094  log2ublem1  22225  log2ublem2  22226  bposlem8  22514  ax5seglem7  23003  ip0i  24047  ip1ilem  24048  ipasslem10  24061  normlem0  24333  polid2i  24381  lnopunilem1  25236  2t6m3t4e0  30581
  Copyright terms: Public domain W3C validator