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  11238  recvguniqlem  11247  resqrexlemover  11263  bdtrilem  11492  bdtri  11493  bcxmas  11742  efsep  11944  efi4p  11970  efival  11985  divalglemnqt  12173  flodddiv4  12189  gcdaddm  12247  pcadd2  12606  4sqlem11  12666  limcimolemlt  15078  tangtx  15252  binom4  15393  2lgslem3c  15514  2lgslem3d  15515