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

Theorem addassi 9100
Description: Associative law for addition. (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
addassi  |-  ( ( A  +  B )  +  C )  =  ( A  +  ( B  +  C ) )

Proof of Theorem addassi
StepHypRef Expression
1 axi.1 . 2  |-  A  e.  CC
2 axi.2 . 2  |-  B  e.  CC
3 axi.3 . 2  |-  C  e.  CC
4 addass 9079 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4mp3an 1280 1  |-  ( ( A  +  B )  +  C )  =  ( A  +  ( B  +  C ) )
Colors of variables: wff set class
Syntax hints:    = wceq 1653    e. wcel 1726  (class class class)co 6083   CCcc 8990    + caddc 8995
This theorem is referenced by:  mul02lem2  9245  addid1  9248  2p2e4  10100  3p2e5  10113  3p3e6  10114  4p2e6  10115  4p3e7  10116  4p4e8  10117  5p2e7  10118  5p3e8  10119  5p4e9  10120  5p5e10  10121  6p2e8  10122  6p3e9  10123  6p4e10  10124  7p2e9  10125  7p3e10  10126  8p2e10  10127  numsuc  10396  nummac  10416  numaddc  10419  6p5lem  10433  binom2i  11492  faclbnd4lem1  11586  gcdaddmlem  13030  mod2xnegi  13409  decexp2  13413  decsplit  13421  lgsdir2lem2  21110  normlem3  22616  stadd3i  23753  ax5seglem7  25876
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addass 9057
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator