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

Theorem addassi 7698
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 7674 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4mp3an 1298 1  |-  ( ( A  +  B )  +  C )  =  ( A  +  ( B  +  C ) )
Colors of variables: wff set class
Syntax hints:    = wceq 1314    e. wcel 1463  (class class class)co 5728   CCcc 7545    + caddc 7550
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-addass 7647
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  2p2e4  8751  3p2e5  8765  3p3e6  8766  4p2e6  8767  4p3e7  8768  4p4e8  8769  5p2e7  8770  5p3e8  8771  5p4e9  8772  6p2e8  8773  6p3e9  8774  7p2e9  8775  numsuc  9099  nummac  9130  numaddc  9133  6p5lem  9155  5p5e10  9156  6p4e10  9157  7p3e10  9160  8p2e10  9165  binom2i  10294  resqrexlemover  10674  3dvdsdec  11410  3dvds2dec  11411
  Copyright terms: Public domain W3C validator