Theorem addassd 8165

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

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200  (class class class)co 6000   CCcc 7993   + caddc 7998

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 8097

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

This theorem is referenced by:  readdcan  8282  muladd11r  8298  cnegexlem1  8317  cnegex  8320  addcan  8322  addcan2  8323  negeu  8333  addsubass  8352  nppcan3  8366  muladd  8526  ltadd2  8562  add1p1  9357  div4p1lem1div2  9361  peano2z  9478  zaddcllempos  9479  zpnn0elfzo1  10409  exbtwnzlemstep  10462  rebtwn2zlemstep  10467  flhalf  10517  flqdiv  10538  binom2  10868  binom3  10874  bernneq  10877  omgadd  11019  ccatass  11138  cvg1nlemres  11491  recvguniqlem  11500  resqrexlemover  11516  bdtrilem  11745  bdtri  11746  bcxmas  11995  efsep  12197  efi4p  12223  efival  12238  divalglemnqt  12426  flodddiv4  12442  gcdaddm  12500  pcadd2  12859  4sqlem11  12919  limcimolemlt  15332  tangtx  15506  binom4  15647  2lgslem3c  15768  2lgslem3d  15769