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

Theorem addassd 7942
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 7904 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4syl3anc 1233 1  |-  ( ph  ->  ( ( A  +  B )  +  C
)  =  ( A  +  ( B  +  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1348    e. wcel 2141  (class class class)co 5853   CCcc 7772    + caddc 7777
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 7876
This theorem depends on definitions:  df-bi 116  df-3an 975
This theorem is referenced by:  readdcan  8059  muladd11r  8075  cnegexlem1  8094  cnegex  8097  addcan  8099  addcan2  8100  negeu  8110  addsubass  8129  nppcan3  8143  muladd  8303  ltadd2  8338  add1p1  9127  div4p1lem1div2  9131  peano2z  9248  zaddcllempos  9249  zpnn0elfzo1  10164  exbtwnzlemstep  10204  rebtwn2zlemstep  10209  flhalf  10258  flqdiv  10277  binom2  10587  binom3  10593  bernneq  10596  omgadd  10737  cvg1nlemres  10949  recvguniqlem  10958  resqrexlemover  10974  bdtrilem  11202  bdtri  11203  bcxmas  11452  efsep  11654  efi4p  11680  efival  11695  divalglemnqt  11879  flodddiv4  11893  gcdaddm  11939  limcimolemlt  13427  tangtx  13553  binom4  13691
  Copyright terms: Public domain W3C validator