Theorem addassd 8349

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 8310	. 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 ) ) )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 8178   + caddc 8183

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-addass 8282

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

This theorem is used by:  readdcan  8468  muladd11r  8484  cnegexlem1  8503  cnegex  8506  addcan  8508  addcan2  8509  negeu  8519  addsubass  8538  nppcan3  8552  muladd  8713  ltadd2  8749  add1p1  9560  div4p1lem1div2  9564  peano2z  9685  zaddcllempos  9686  zpnn0elfzo1  10637  exbtwnzlemstep  10693  rebtwn2zlemstep  10698  flhalf  10752  flqdiv  10773  binom2  11103  binom3  11109  bernneq  11113  omgadd  11258  ccatass  11392  cvg1nlemres  11767  recvguniqlem  11776  resqrexlemover  11792  bdtrilem  12024  bdtri  12025  bcxmas  12275  efsep  12477  efi4p  12503  efival  12518  divalglemnqt  12706  flodddiv4  12722  gcdaddm  12780  pcadd2  13143  4sqlem11  13203  limcimolemlt  15856  tangtx  16031  logfac  16090  binom4  16180  ppiqub  16254  bcp1ctr  16267  bposlem9  16280  2lgslem3c  16380  2lgslem3d  16381  qdiff  17265