Theorem addassd 8044

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 8004	. 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 2164  (class class class)co 5919   CCcc 7872   + caddc 7877

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 7976

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

This theorem is referenced by:  readdcan  8161  muladd11r  8177  cnegexlem1  8196  cnegex  8199  addcan  8201  addcan2  8202  negeu  8212  addsubass  8231  nppcan3  8245  muladd  8405  ltadd2  8440  add1p1  9235  div4p1lem1div2  9239  peano2z  9356  zaddcllempos  9357  zpnn0elfzo1  10278  exbtwnzlemstep  10319  rebtwn2zlemstep  10324  flhalf  10374  flqdiv  10395  binom2  10725  binom3  10731  bernneq  10734  omgadd  10876  cvg1nlemres  11132  recvguniqlem  11141  resqrexlemover  11157  bdtrilem  11385  bdtri  11386  bcxmas  11635  efsep  11837  efi4p  11863  efival  11878  divalglemnqt  12064  flodddiv4  12078  gcdaddm  12124  pcadd2  12482  4sqlem11  12542  limcimolemlt  14843  tangtx  15014  binom4  15152  2lgslem3c  15252  2lgslem3d  15253