Theorem addassd 8201

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

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2202  (class class class)co 6017   CCcc 8029   + caddc 8034

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 8133

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

This theorem is referenced by:  readdcan  8318  muladd11r  8334  cnegexlem1  8353  cnegex  8356  addcan  8358  addcan2  8359  negeu  8369  addsubass  8388  nppcan3  8402  muladd  8562  ltadd2  8598  add1p1  9393  div4p1lem1div2  9397  peano2z  9514  zaddcllempos  9515  zpnn0elfzo1  10452  exbtwnzlemstep  10506  rebtwn2zlemstep  10511  flhalf  10561  flqdiv  10582  binom2  10912  binom3  10918  bernneq  10921  omgadd  11064  ccatass  11184  cvg1nlemres  11545  recvguniqlem  11554  resqrexlemover  11570  bdtrilem  11799  bdtri  11800  bcxmas  12049  efsep  12251  efi4p  12277  efival  12292  divalglemnqt  12480  flodddiv4  12496  gcdaddm  12554  pcadd2  12913  4sqlem11  12973  limcimolemlt  15387  tangtx  15561  binom4  15702  2lgslem3c  15823  2lgslem3d  15824