Theorem addassd 7921

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

Syntax hints:   -> wi 4   = wceq 1343   e. wcel 2136  (class class class)co 5842   CCcc 7751   + caddc 7756

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-addass 7855

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  readdcan  8038  muladd11r  8054  cnegexlem1  8073  cnegex  8076  addcan  8078  addcan2  8079  negeu  8089  addsubass  8108  nppcan3  8122  muladd  8282  ltadd2  8317  add1p1  9106  div4p1lem1div2  9110  peano2z  9227  zaddcllempos  9228  zpnn0elfzo1  10143  exbtwnzlemstep  10183  rebtwn2zlemstep  10188  flhalf  10237  flqdiv  10256  binom2  10566  binom3  10572  bernneq  10575  omgadd  10715  cvg1nlemres  10927  recvguniqlem  10936  resqrexlemover  10952  bdtrilem  11180  bdtri  11181  bcxmas  11430  efsep  11632  efi4p  11658  efival  11673  divalglemnqt  11857  flodddiv4  11871  gcdaddm  11917  limcimolemlt  13273  tangtx  13399  binom4  13537