Theorem addassd 8348

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 8177   + caddc 8182

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-addass 8281

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  readdcan  8466  muladd11r  8482  cnegexlem1  8501  cnegex  8504  addcan  8506  addcan2  8507  negeu  8517  addsubass  8536  nppcan3  8550  muladd  8711  ltadd2  8747  add1p1  9555  div4p1lem1div2  9559  peano2z  9680  zaddcllempos  9681  zpnn0elfzo1  10626  exbtwnzlemstep  10682  rebtwn2zlemstep  10687  flhalf  10737  flqdiv  10758  binom2  11088  binom3  11094  bernneq  11098  omgadd  11242  ccatass  11376  cvg1nlemres  11751  recvguniqlem  11760  resqrexlemover  11776  bdtrilem  12005  bdtri  12006  bcxmas  12256  efsep  12458  efi4p  12484  efival  12499  divalglemnqt  12687  flodddiv4  12703  gcdaddm  12761  pcadd2  13120  4sqlem11  13180  limcimolemlt  15765  tangtx  15939  logfac  15995  binom4  16081  2lgslem3c  16214  2lgslem3d  16215  qdiff  17098