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

Theorem addassd 7902
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 7864 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4syl3anc 1220 1  |-  ( ph  ->  ( ( A  +  B )  +  C
)  =  ( A  +  ( B  +  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1335    e. wcel 2128  (class class class)co 5826   CCcc 7732    + caddc 7737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-addass 7836
This theorem depends on definitions:  df-bi 116  df-3an 965
This theorem is referenced by:  readdcan  8019  muladd11r  8035  cnegexlem1  8054  cnegex  8057  addcan  8059  addcan2  8060  negeu  8070  addsubass  8089  nppcan3  8103  muladd  8263  ltadd2  8298  add1p1  9087  div4p1lem1div2  9091  peano2z  9208  zaddcllempos  9209  zpnn0elfzo1  10116  exbtwnzlemstep  10156  rebtwn2zlemstep  10161  flhalf  10210  flqdiv  10229  binom2  10538  binom3  10544  bernneq  10547  omgadd  10687  cvg1nlemres  10896  recvguniqlem  10905  resqrexlemover  10921  bdtrilem  11149  bdtri  11150  bcxmas  11397  efsep  11599  efi4p  11625  efival  11640  divalglemnqt  11823  flodddiv4  11837  gcdaddm  11883  limcimolemlt  13103  tangtx  13229  binom4  13367
  Copyright terms: Public domain W3C validator