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

Theorem addassi 9382
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 9357 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4mp3an 1307 1  |-  ( ( A  +  B )  +  C )  =  ( A  +  ( B  +  C ) )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1362    e. wcel 1755  (class class class)co 6080   CCcc 9268    + caddc 9273
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 9335
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 960
This theorem is referenced by:  mul02lem2  9534  addid1  9537  2p2e4  10427  3p2e5  10442  3p3e6  10443  4p2e6  10444  4p3e7  10445  4p4e8  10446  5p2e7  10447  5p3e8  10448  5p4e9  10449  5p5e10  10450  6p2e8  10451  6p3e9  10452  6p4e10  10453  7p2e9  10454  7p3e10  10455  8p2e10  10456  numsuc  10755  nummac  10775  numaddc  10778  6p5lem  10792  binom2i  11959  faclbnd4lem1  12053  gcdaddmlem  13695  mod2xnegi  14083  decexp2  14087  decsplit  14095  lgsdir2lem2  22548  ax5seglem7  23004  normlem3  24337  stadd3i  25475
  Copyright terms: Public domain W3C validator