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

Theorem addassi 9651
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 9626 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4mp3an 1360 1  |-  ( ( A  +  B )  +  C )  =  ( A  +  ( B  +  C ) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    e. wcel 1868  (class class class)co 6301   CCcc 9537    + caddc 9542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 9604
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984
This theorem is referenced by:  mul02lem2  9810  addid1  9813  2p2e4  10727  3p2e5  10742  3p3e6  10743  4p2e6  10744  4p3e7  10745  4p4e8  10746  5p2e7  10747  5p3e8  10748  5p4e9  10749  5p5e10  10750  6p2e8  10751  6p3e9  10752  6p4e10  10753  7p2e9  10754  7p3e10  10755  8p2e10  10756  numsuc  11063  nummac  11083  numaddc  11086  6p5lem  11100  binom2i  12383  faclbnd4lem1  12477  gcdaddmlem  14479  mod2xnegi  15030  decexp2  15034  decsplit  15042  lgsdir2lem2  24238  ax5seglem7  24951  normlem3  26750  stadd3i  27886  quad3  30297  unitadd  36499  sqwvfoura  37911  sqwvfourb  37912  fouriersw  37914  bgoldbtbndlem1  38611  3exp4mod41  38627
  Copyright terms: Public domain W3C validator