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  8467  muladd11r  8483  cnegexlem1  8502  cnegex  8505  addcan  8507  addcan2  8508  negeu  8518  addsubass  8537  nppcan3  8551  muladd  8712  ltadd2  8748  add1p1  9559  div4p1lem1div2  9563  peano2z  9684  zaddcllempos  9685  zpnn0elfzo1  10636  exbtwnzlemstep  10692  rebtwn2zlemstep  10697  flhalf  10750  flqdiv  10771  binom2  11101  binom3  11107  bernneq  11111  omgadd  11256  ccatass  11390  cvg1nlemres  11765  recvguniqlem  11774  resqrexlemover  11790  bdtrilem  12021  bdtri  12022  bcxmas  12272  efsep  12474  efi4p  12500  efival  12515  divalglemnqt  12703  flodddiv4  12719  gcdaddm  12777  pcadd2  13140  4sqlem11  13200  limcimolemlt  15814  tangtx  15989  logfac  16048  binom4  16138  ppiqub  16194  bcp1ctr  16204  2lgslem3c  16312  2lgslem3d  16313  qdiff  17196