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

Theorem adddii 8863
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 8842 . 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 1632    e. wcel 1696  (class class class)co 5874   CCcc 8751    + caddc 8756    x. cmul 8758
This theorem is referenced by:  addid1  9008  3t3e9  9889  numltc  10160  numsucc  10166  numma  10171  4t3lem  10211  decbin2  10244  binom2i  11228  faclbnd4lem1  11322  mod2xnegi  13102  decsplit  13114  log2ublem1  20258  log2ublem2  20259  bposlem8  20546  ip0i  21419  ip1ilem  21420  ipasslem10  21433  normlem0  21704  polid2i  21752  lnopunilem1  22606  ax5seglem7  24635
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-distr 8820
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator