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

Theorem addassi 7967
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 7943 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4mp3an 1337 1  |-  ( ( A  +  B )  +  C )  =  ( A  +  ( B  +  C ) )
Colors of variables: wff set class
Syntax hints:    = wceq 1353    e. wcel 2148  (class class class)co 5877   CCcc 7811    + caddc 7816
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 7915
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  2p2e4  9048  3p2e5  9062  3p3e6  9063  4p2e6  9064  4p3e7  9065  4p4e8  9066  5p2e7  9067  5p3e8  9068  5p4e9  9069  6p2e8  9070  6p3e9  9071  7p2e9  9072  numsuc  9399  nummac  9430  numaddc  9433  6p5lem  9455  5p5e10  9456  6p4e10  9457  7p3e10  9460  8p2e10  9465  binom2i  10631  resqrexlemover  11021  3dvdsdec  11872  3dvds2dec  11873  lgsdir2lem2  14515  2lgsoddprmlem3d  14543
  Copyright terms: Public domain W3C validator