Theorem addassd 8338

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

Step	Hyp	Ref	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 8299	. 2 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
5	1, 2, 3, 4	syl3anc 1278	1 |- ( ph -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )

Syntax hints:   -> wi 4   = wceq 1402   e. wcel 2209  (class class class)co 6075   CCcc 8167   + caddc 8172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-addass 8271

This theorem depends on definitions:  df-bi 117  df-3an 1011

This theorem is referenced by:  readdcan  8456  muladd11r  8472  cnegexlem1  8491  cnegex  8494  addcan  8496  addcan2  8497  negeu  8507  addsubass  8526  nppcan3  8540  muladd  8701  ltadd2  8737  add1p1  9534  div4p1lem1div2  9538  peano2z  9659  zaddcllempos  9660  zpnn0elfzo1  10604  exbtwnzlemstep  10660  rebtwn2zlemstep  10665  flhalf  10715  flqdiv  10736  binom2  11066  binom3  11072  bernneq  11076  omgadd  11220  ccatass  11354  cvg1nlemres  11729  recvguniqlem  11738  resqrexlemover  11754  bdtrilem  11983  bdtri  11984  bcxmas  12234  efsep  12436  efi4p  12462  efival  12477  divalglemnqt  12665  flodddiv4  12681  gcdaddm  12739  pcadd2  13098  4sqlem11  13158  limcimolemlt  15688  tangtx  15862  logfac  15918  binom4  16004  2lgslem3c  16128  2lgslem3d  16129  qdiff  17003