ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  addassi Unicode version

Theorem addassi 7979
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 7955 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4mp3an 1347 1  |-  ( ( A  +  B )  +  C )  =  ( A  +  ( B  +  C ) )
Colors of variables: wff set class
Syntax hints:    = wceq 1363    e. wcel 2158  (class class class)co 5888   CCcc 7823    + caddc 7828
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-addass 7927
This theorem depends on definitions:  df-bi 117  df-3an 981
This theorem is referenced by:  2p2e4  9060  3p2e5  9074  3p3e6  9075  4p2e6  9076  4p3e7  9077  4p4e8  9078  5p2e7  9079  5p3e8  9080  5p4e9  9081  6p2e8  9082  6p3e9  9083  7p2e9  9084  numsuc  9411  nummac  9442  numaddc  9445  6p5lem  9467  5p5e10  9468  6p4e10  9469  7p3e10  9472  8p2e10  9477  binom2i  10643  resqrexlemover  11033  3dvdsdec  11884  3dvds2dec  11885  lgsdir2lem2  14726  2lgsoddprmlem3d  14754
  Copyright terms: Public domain W3C validator