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

Theorem addassd 7982
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 7943 . 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 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:  readdcan  8099  muladd11r  8115  cnegexlem1  8134  cnegex  8137  addcan  8139  addcan2  8140  negeu  8150  addsubass  8169  nppcan3  8183  muladd  8343  ltadd2  8378  add1p1  9170  div4p1lem1div2  9174  peano2z  9291  zaddcllempos  9292  zpnn0elfzo1  10210  exbtwnzlemstep  10250  rebtwn2zlemstep  10255  flhalf  10304  flqdiv  10323  binom2  10634  binom3  10640  bernneq  10643  omgadd  10784  cvg1nlemres  10996  recvguniqlem  11005  resqrexlemover  11021  bdtrilem  11249  bdtri  11250  bcxmas  11499  efsep  11701  efi4p  11727  efival  11742  divalglemnqt  11927  flodddiv4  11941  gcdaddm  11987  limcimolemlt  14172  tangtx  14298  binom4  14436
  Copyright terms: Public domain W3C validator