Theorem addassd 8049

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

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2167  (class class class)co 5922   CCcc 7877   + caddc 7882

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 7981

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

This theorem is referenced by:  readdcan  8166  muladd11r  8182  cnegexlem1  8201  cnegex  8204  addcan  8206  addcan2  8207  negeu  8217  addsubass  8236  nppcan3  8250  muladd  8410  ltadd2  8446  add1p1  9241  div4p1lem1div2  9245  peano2z  9362  zaddcllempos  9363  zpnn0elfzo1  10284  exbtwnzlemstep  10337  rebtwn2zlemstep  10342  flhalf  10392  flqdiv  10413  binom2  10743  binom3  10749  bernneq  10752  omgadd  10894  cvg1nlemres  11150  recvguniqlem  11159  resqrexlemover  11175  bdtrilem  11404  bdtri  11405  bcxmas  11654  efsep  11856  efi4p  11882  efival  11897  divalglemnqt  12085  flodddiv4  12101  gcdaddm  12151  pcadd2  12510  4sqlem11  12570  limcimolemlt  14900  tangtx  15074  binom4  15215  2lgslem3c  15336  2lgslem3d  15337