Theorem addassd 8192

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

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200  (class class class)co 6013   CCcc 8020   + caddc 8025

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 8124

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

This theorem is referenced by:  readdcan  8309  muladd11r  8325  cnegexlem1  8344  cnegex  8347  addcan  8349  addcan2  8350  negeu  8360  addsubass  8379  nppcan3  8393  muladd  8553  ltadd2  8589  add1p1  9384  div4p1lem1div2  9388  peano2z  9505  zaddcllempos  9506  zpnn0elfzo1  10443  exbtwnzlemstep  10497  rebtwn2zlemstep  10502  flhalf  10552  flqdiv  10573  binom2  10903  binom3  10909  bernneq  10912  omgadd  11055  ccatass  11175  cvg1nlemres  11536  recvguniqlem  11545  resqrexlemover  11561  bdtrilem  11790  bdtri  11791  bcxmas  12040  efsep  12242  efi4p  12268  efival  12283  divalglemnqt  12471  flodddiv4  12487  gcdaddm  12545  pcadd2  12904  4sqlem11  12964  limcimolemlt  15378  tangtx  15552  binom4  15693  2lgslem3c  15814  2lgslem3d  15815