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

Theorem addassd 7976
Description: Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1  |-  ( ph  ->  A  e.  CC )
addcld.2  |-  ( ph  ->  B  e.  CC )
addassd.3  |-  ( ph  ->  C  e.  CC )
Assertion
Ref Expression
addassd  |-  ( ph  ->  ( ( A  +  B )  +  C
)  =  ( A  +  ( B  +  C ) ) )

Proof of Theorem addassd
StepHypRef Expression
1 addcld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addcld.2 . 2  |-  ( ph  ->  B  e.  CC )
3 addassd.3 . 2  |-  ( ph  ->  C  e.  CC )
4 addass 7938 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4syl3anc 1238 1  |-  ( ph  ->  ( ( A  +  B )  +  C
)  =  ( A  +  ( B  +  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1353    e. wcel 2148  (class class class)co 5872   CCcc 7806    + caddc 7811
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 7910
This theorem depends on definitions:  df-bi 117  df-3an 980
This theorem is referenced by:  readdcan  8093  muladd11r  8109  cnegexlem1  8128  cnegex  8131  addcan  8133  addcan2  8134  negeu  8144  addsubass  8163  nppcan3  8177  muladd  8337  ltadd2  8372  add1p1  9164  div4p1lem1div2  9168  peano2z  9285  zaddcllempos  9286  zpnn0elfzo1  10203  exbtwnzlemstep  10243  rebtwn2zlemstep  10248  flhalf  10297  flqdiv  10316  binom2  10626  binom3  10632  bernneq  10635  omgadd  10775  cvg1nlemres  10987  recvguniqlem  10996  resqrexlemover  11012  bdtrilem  11240  bdtri  11241  bcxmas  11490  efsep  11692  efi4p  11718  efival  11733  divalglemnqt  11917  flodddiv4  11931  gcdaddm  11977  limcimolemlt  14004  tangtx  14130  binom4  14268
  Copyright terms: Public domain W3C validator