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

Theorem addassi 9098
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 9077 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4mp3an 1279 1  |-  ( ( A  +  B )  +  C )  =  ( A  +  ( B  +  C ) )
Colors of variables: wff set class
Syntax hints:    = wceq 1652    e. wcel 1725  (class class class)co 6081   CCcc 8988    + caddc 8993
This theorem is referenced by:  mul02lem2  9243  addid1  9246  2p2e4  10098  3p2e5  10111  3p3e6  10112  4p2e6  10113  4p3e7  10114  4p4e8  10115  5p2e7  10116  5p3e8  10117  5p4e9  10118  5p5e10  10119  6p2e8  10120  6p3e9  10121  6p4e10  10122  7p2e9  10123  7p3e10  10124  8p2e10  10125  numsuc  10394  nummac  10414  numaddc  10417  6p5lem  10431  binom2i  11490  faclbnd4lem1  11584  gcdaddmlem  13028  mod2xnegi  13407  decexp2  13411  decsplit  13419  lgsdir2lem2  21108  normlem3  22614  stadd3i  23751  ax5seglem7  25874
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addass 9055
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator