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

Theorem addassi 9497
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 9472 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4mp3an 1315 1  |-  ( ( A  +  B )  +  C )  =  ( A  +  ( B  +  C ) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370    e. wcel 1758  (class class class)co 6192   CCcc 9383    + caddc 9388
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 9450
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967
This theorem is referenced by:  mul02lem2  9649  addid1  9652  2p2e4  10542  3p2e5  10557  3p3e6  10558  4p2e6  10559  4p3e7  10560  4p4e8  10561  5p2e7  10562  5p3e8  10563  5p4e9  10564  5p5e10  10565  6p2e8  10566  6p3e9  10567  6p4e10  10568  7p2e9  10569  7p3e10  10570  8p2e10  10571  numsuc  10870  nummac  10890  numaddc  10893  6p5lem  10907  binom2i  12078  faclbnd4lem1  12172  gcdaddmlem  13816  mod2xnegi  14204  decexp2  14208  decsplit  14216  lgsdir2lem2  22781  ax5seglem7  23318  normlem3  24651  stadd3i  25789  quad3  27439
  Copyright terms: Public domain W3C validator