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

Theorem addassd 7049
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 7011 . 2  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
51, 2, 3, 4syl3anc 1135 1  |-  ( ph  ->  ( ( A  +  B )  +  C
)  =  ( A  +  ( B  +  C ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1243    e. wcel 1393  (class class class)co 5512   CCcc 6887    + caddc 6892
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-addass 6986
This theorem depends on definitions:  df-bi 110  df-3an 887
This theorem is referenced by:  readdcan  7153  cnegexlem1  7186  cnegex  7189  addcan  7191  addcan2  7192  negeu  7202  addsubass  7221  nppcan3  7235  muladd  7381  ltadd2  7416  add1p1  8174  div4p1lem1div2  8177  peano2z  8281  zaddcllempos  8282  zpnn0elfzo1  9064  qbtwnzlemstep  9103  rebtwn2zlemstep  9107  flhalf  9144  flqdiv  9163  binom2  9362  binom3  9366  bernneq  9369  cvg1nlemres  9584  recvguniqlem  9592  resqrexlemover  9608
  Copyright terms: Public domain W3C validator