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  9689  zaddcllempos  9690  zpnn0elfzo1  10642  exbtwnzlemstep  10698  rebtwn2zlemstep  10703  flhalf  10757  flqdiv  10778  binom2  11108  binom3  11114  bernneq  11118  omgadd  11263  ccatass  11397  cvg1nlemres  11772  recvguniqlem  11781  resqrexlemover  11797  bdtrilem  12029  bdtri  12030  bcxmas  12280  efsep  12482  efi4p  12508  efival  12523  divalglemnqt  12711  flodddiv4  12727  gcdaddm  12785  pcadd2  13148  4sqlem11  13208  limcimolemlt  15907  tangtx  16082  logfac  16143  binom4  16236  ppiqub  16310  bcp1ctr  16323  bposlem9  16336  2lgslem3c  16436  2lgslem3d  16437  qdiff  17322