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

Theorem addassi 8845
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 8824 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4mp3an 1277 1  |-  ( ( A  +  B )  +  C )  =  ( A  +  ( B  +  C ) )
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1684  (class class class)co 5858   CCcc 8735    + caddc 8740
This theorem is referenced by:  mul02lem2  8989  addid1  8992  2p2e4  9842  3p2e5  9855  3p3e6  9856  4p2e6  9857  4p3e7  9858  4p4e8  9859  5p2e7  9860  5p3e8  9861  5p4e9  9862  5p5e10  9863  6p2e8  9864  6p3e9  9865  6p4e10  9866  7p2e9  9867  7p3e10  9868  8p2e10  9869  numsuc  10136  nummac  10156  numaddc  10159  6p5lem  10173  binom2i  11212  faclbnd4lem1  11306  gcdaddmlem  12707  mod2xnegi  13086  decexp2  13090  decsplit  13098  lgsdir2lem2  20563  normlem3  21691  stadd3i  22828  ax5seglem7  23974  3timesi  24590
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addass 8802
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator