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

Theorem addassi 7475
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 7451 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4mp3an 1273 1  |-  ( ( A  +  B )  +  C )  =  ( A  +  ( B  +  C ) )
Colors of variables: wff set class
Syntax hints:    = wceq 1289    e. wcel 1438  (class class class)co 5634   CCcc 7327    + caddc 7332
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-addass 7426
This theorem depends on definitions:  df-bi 115  df-3an 926
This theorem is referenced by:  2p2e4  8513  3p2e5  8527  3p3e6  8528  4p2e6  8529  4p3e7  8530  4p4e8  8531  5p2e7  8532  5p3e8  8533  5p4e9  8534  6p2e8  8535  6p3e9  8536  7p2e9  8537  numsuc  8859  nummac  8890  numaddc  8893  6p5lem  8915  5p5e10  8916  6p4e10  8917  7p3e10  8920  8p2e10  8925  binom2i  10028  resqrexlemover  10408  3dvdsdec  10958  3dvds2dec  10959
  Copyright terms: Public domain W3C validator