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

Theorem addassi 9593
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 9568 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4mp3an 1322 1  |-  ( ( A  +  B )  +  C )  =  ( A  +  ( B  +  C ) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1398    e. wcel 1823  (class class class)co 6270   CCcc 9479    + caddc 9484
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 9546
This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973
This theorem is referenced by:  mul02lem2  9746  addid1  9749  2p2e4  10649  3p2e5  10664  3p3e6  10665  4p2e6  10666  4p3e7  10667  4p4e8  10668  5p2e7  10669  5p3e8  10670  5p4e9  10671  5p5e10  10672  6p2e8  10673  6p3e9  10674  6p4e10  10675  7p2e9  10676  7p3e10  10677  8p2e10  10678  numsuc  10988  nummac  11008  numaddc  11011  6p5lem  11025  binom2i  12262  faclbnd4lem1  12356  gcdaddmlem  14253  mod2xnegi  14644  decexp2  14648  decsplit  14656  lgsdir2lem2  23800  ax5seglem7  24443  normlem3  26230  stadd3i  27368  quad3  29291  sqwvfoura  32253  sqwvfourb  32254  fouriersw  32256  3exp4mod41  32622  unitadd  38547
  Copyright terms: Public domain W3C validator