Theorem addassd 8202

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

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2202  (class class class)co 6018   CCcc 8030   + caddc 8035

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 8134

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

This theorem is referenced by:  readdcan  8319  muladd11r  8335  cnegexlem1  8354  cnegex  8357  addcan  8359  addcan2  8360  negeu  8370  addsubass  8389  nppcan3  8403  muladd  8563  ltadd2  8599  add1p1  9394  div4p1lem1div2  9398  peano2z  9515  zaddcllempos  9516  zpnn0elfzo1  10454  exbtwnzlemstep  10508  rebtwn2zlemstep  10513  flhalf  10563  flqdiv  10584  binom2  10914  binom3  10920  bernneq  10923  omgadd  11066  ccatass  11189  cvg1nlemres  11563  recvguniqlem  11572  resqrexlemover  11588  bdtrilem  11817  bdtri  11818  bcxmas  12068  efsep  12270  efi4p  12296  efival  12311  divalglemnqt  12499  flodddiv4  12515  gcdaddm  12573  pcadd2  12932  4sqlem11  12992  limcimolemlt  15407  tangtx  15581  binom4  15722  2lgslem3c  15843  2lgslem3d  15844  qdiff  16704