Theorem addassd 8115

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

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2177  (class class class)co 5957   CCcc 7943   + caddc 7948

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 8047

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

This theorem is referenced by:  readdcan  8232  muladd11r  8248  cnegexlem1  8267  cnegex  8270  addcan  8272  addcan2  8273  negeu  8283  addsubass  8302  nppcan3  8316  muladd  8476  ltadd2  8512  add1p1  9307  div4p1lem1div2  9311  peano2z  9428  zaddcllempos  9429  zpnn0elfzo1  10359  exbtwnzlemstep  10412  rebtwn2zlemstep  10417  flhalf  10467  flqdiv  10488  binom2  10818  binom3  10824  bernneq  10827  omgadd  10969  ccatass  11087  cvg1nlemres  11371  recvguniqlem  11380  resqrexlemover  11396  bdtrilem  11625  bdtri  11626  bcxmas  11875  efsep  12077  efi4p  12103  efival  12118  divalglemnqt  12306  flodddiv4  12322  gcdaddm  12380  pcadd2  12739  4sqlem11  12799  limcimolemlt  15211  tangtx  15385  binom4  15526  2lgslem3c  15647  2lgslem3d  15648