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

Theorem addassd 7203
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 7165 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4syl3anc 1170 1  |-  ( ph  ->  ( ( A  +  B )  +  C
)  =  ( A  +  ( B  +  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1285    e. wcel 1434  (class class class)co 5543   CCcc 7041    + caddc 7046
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 7140
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  readdcan  7315  muladd11r  7331  cnegexlem1  7350  cnegex  7353  addcan  7355  addcan2  7356  negeu  7366  addsubass  7385  nppcan3  7399  muladd  7555  ltadd2  7590  add1p1  8347  div4p1lem1div2  8351  peano2z  8468  zaddcllempos  8469  zpnn0elfzo1  9294  exbtwnzlemstep  9334  rebtwn2zlemstep  9339  flhalf  9384  flqdiv  9403  binom2  9682  binom3  9687  bernneq  9690  omgadd  9826  cvg1nlemres  10009  recvguniqlem  10018  resqrexlemover  10034  divalglemnqt  10464  flodddiv4  10478  gcdaddm  10519
  Copyright terms: Public domain W3C validator