Theorem addassd 8354

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 8315	. 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 6088   CCcc 8183   + caddc 8188

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 8287

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

This theorem is used by:  readdcan  8473  muladd11r  8489  cnegexlem1  8508  cnegex  8511  addcan  8513  addcan2  8514  negeu  8524  addsubass  8543  nppcan3  8557  muladd  8718  ltadd2  8754  add1p1  9566  div4p1lem1div2  9570  peano2z  9691  zaddcllempos  9692  zpnn0elfzo1  10643  exbtwnzlemstep  10699  rebtwn2zlemstep  10704  flhalf  10758  flqdiv  10779  binom2  11109  binom3  11115  bernneq  11119  omgadd  11264  ccatass  11398  cvg1nlemres  11773  recvguniqlem  11782  resqrexlemover  11798  bdtrilem  12030  bdtri  12031  bcxmas  12281  efsep  12483  efi4p  12509  efival  12524  divalglemnqt  12712  flodddiv4  12728  gcdaddm  12786  pcadd2  13149  4sqlem11  13209  limcimolemlt  15890  tangtx  16065  logfac  16126  binom4  16219  ppiqub  16293  bcp1ctr  16306  bposlem9  16319  2lgslem3c  16419  2lgslem3d  16420  qdiff  17305