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

Theorem adddii 9602
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 9577 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
51, 2, 3, 4mp3an 1324 1  |-  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379    e. wcel 1767  (class class class)co 6282   CCcc 9486    + caddc 9491    x. cmul 9493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-distr 9555
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
This theorem is referenced by:  addid1  9755  3t3e9  10684  numltc  10992  numsucc  10998  numma  11003  4t3lem  11043  decbin2  11076  binom2i  12241  faclbnd4lem1  12335  mod2xnegi  14412  decsplit  14424  log2ublem1  23005  log2ublem2  23006  bposlem8  23294  ax5seglem7  23914  ip0i  25416  ip1ilem  25417  ipasslem10  25430  normlem0  25702  polid2i  25750  lnopunilem1  26605  fourierswlem  31531  2t6m3t4e0  32001
  Copyright terms: Public domain W3C validator