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

Theorem adddii 9653
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 9628 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
51, 2, 3, 4mp3an 1360 1  |-  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    e. wcel 1868  (class class class)co 6301   CCcc 9537    + caddc 9542    x. cmul 9544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 9606
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984
This theorem is referenced by:  addid1  9813  3t3e9  10762  numltc  11071  numsucc  11077  numma  11082  4t3lem  11122  decbin2  11155  binom2i  12383  faclbnd4lem1  12477  mod2xnegi  15028  decsplit  15040  log2ublem1  23856  log2ublem2  23857  bposlem8  24203  ax5seglem7  24949  ip0i  26449  ip1ilem  26450  ipasslem10  26463  normlem0  26745  polid2i  26793  lnopunilem1  27646  fourierswlem  37911  3exp4mod41  38625  2t6m3t4e0  39317
  Copyright terms: Public domain W3C validator