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

Theorem adddii 9100
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 9079 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) ) )
51, 2, 3, 4mp3an 1279 1  |-  ( A  x.  ( B  +  C ) )  =  ( ( A  x.  B )  +  ( A  x.  C ) )
Colors of variables: wff set class
Syntax hints:    = wceq 1652    e. wcel 1725  (class class class)co 6081   CCcc 8988    + caddc 8993    x. cmul 8995
This theorem is referenced by:  addid1  9246  3t3e9  10129  numltc  10402  numsucc  10408  numma  10413  4t3lem  10453  decbin2  10486  binom2i  11490  faclbnd4lem1  11584  mod2xnegi  13407  decsplit  13419  log2ublem1  20786  log2ublem2  20787  bposlem8  21075  ip0i  22326  ip1ilem  22327  ipasslem10  22340  normlem0  22611  polid2i  22659  lnopunilem1  23513  ax5seglem7  25874
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-distr 9057
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator