Theorem addassd 8094

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

Syntax hints:   -> wi 4   = wceq 1372   e. wcel 2175  (class class class)co 5943   CCcc 7922   + caddc 7927

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 8026

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

This theorem is referenced by:  readdcan  8211  muladd11r  8227  cnegexlem1  8246  cnegex  8249  addcan  8251  addcan2  8252  negeu  8262  addsubass  8281  nppcan3  8295  muladd  8455  ltadd2  8491  add1p1  9286  div4p1lem1div2  9290  peano2z  9407  zaddcllempos  9408  zpnn0elfzo1  10335  exbtwnzlemstep  10388  rebtwn2zlemstep  10393  flhalf  10443  flqdiv  10464  binom2  10794  binom3  10800  bernneq  10803  omgadd  10945  ccatass  11062  cvg1nlemres  11267  recvguniqlem  11276  resqrexlemover  11292  bdtrilem  11521  bdtri  11522  bcxmas  11771  efsep  11973  efi4p  11999  efival  12014  divalglemnqt  12202  flodddiv4  12218  gcdaddm  12276  pcadd2  12635  4sqlem11  12695  limcimolemlt  15107  tangtx  15281  binom4  15422  2lgslem3c  15543  2lgslem3d  15544