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

Theorem addassi 8861
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 8840 . 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 1632    e. wcel 1696  (class class class)co 5874   CCcc 8751    + caddc 8756
This theorem is referenced by:  mul02lem2  9005  addid1  9008  2p2e4  9858  3p2e5  9871  3p3e6  9872  4p2e6  9873  4p3e7  9874  4p4e8  9875  5p2e7  9876  5p3e8  9877  5p4e9  9878  5p5e10  9879  6p2e8  9880  6p3e9  9881  6p4e10  9882  7p2e9  9883  7p3e10  9884  8p2e10  9885  numsuc  10152  nummac  10172  numaddc  10175  6p5lem  10189  binom2i  11228  faclbnd4lem1  11322  gcdaddmlem  12723  mod2xnegi  13102  decexp2  13106  decsplit  13114  lgsdir2lem2  20579  normlem3  21707  stadd3i  22844  ax5seglem7  24635  3timesi  25281
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-addass 8818
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator