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

Theorem addassd 7510
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 7472 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4syl3anc 1174 1  |-  ( ph  ->  ( ( A  +  B )  +  C
)  =  ( A  +  ( B  +  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1289    e. wcel 1438  (class class class)co 5652   CCcc 7348    + caddc 7353
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-addass 7447
This theorem depends on definitions:  df-bi 115  df-3an 926
This theorem is referenced by:  readdcan  7622  muladd11r  7638  cnegexlem1  7657  cnegex  7660  addcan  7662  addcan2  7663  negeu  7673  addsubass  7692  nppcan3  7706  muladd  7862  ltadd2  7897  add1p1  8665  div4p1lem1div2  8669  peano2z  8786  zaddcllempos  8787  zpnn0elfzo1  9619  exbtwnzlemstep  9659  rebtwn2zlemstep  9664  flhalf  9709  flqdiv  9728  binom2  10065  binom3  10071  bernneq  10074  omgadd  10210  cvg1nlemres  10418  recvguniqlem  10427  resqrexlemover  10443  bcxmas  10883  efsep  10981  efi4p  11008  efival  11023  divalglemnqt  11198  flodddiv4  11212  gcdaddm  11253
  Copyright terms: Public domain W3C validator