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

Theorem addassi 9062
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 9041 . 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 1649    e. wcel 1721  (class class class)co 6048   CCcc 8952    + caddc 8957
This theorem is referenced by:  mul02lem2  9207  addid1  9210  2p2e4  10062  3p2e5  10075  3p3e6  10076  4p2e6  10077  4p3e7  10078  4p4e8  10079  5p2e7  10080  5p3e8  10081  5p4e9  10082  5p5e10  10083  6p2e8  10084  6p3e9  10085  6p4e10  10086  7p2e9  10087  7p3e10  10088  8p2e10  10089  numsuc  10358  nummac  10378  numaddc  10381  6p5lem  10395  binom2i  11453  faclbnd4lem1  11547  gcdaddmlem  12991  mod2xnegi  13370  decexp2  13374  decsplit  13382  lgsdir2lem2  21069  normlem3  22575  stadd3i  23712  ax5seglem7  25786
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addass 9019
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator