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

Theorem adddii 8847
Description: Distributive law. (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 8826 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
51, 2, 3, 4mp3an 1277 1  |-  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) )
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1684  (class class class)co 5858   CCcc 8735    + caddc 8740    x. cmul 8742
This theorem is referenced by:  addid1  8992  3t3e9  9873  numltc  10144  numsucc  10150  numma  10155  4t3lem  10195  decbin2  10228  binom2i  11212  faclbnd4lem1  11306  mod2xnegi  13086  decsplit  13098  log2ublem1  20242  log2ublem2  20243  bposlem8  20530  ip0i  21403  ip1ilem  21404  ipasslem10  21417  normlem0  21688  polid2i  21736  lnopunilem1  22590  ax5seglem7  24563
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-distr 8804
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator