Theorem addassd 8312

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2205  (class class class)co 6058   CCcc 8141   + caddc 8146

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 8245

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

This theorem is referenced by:  readdcan  8429  muladd11r  8445  cnegexlem1  8464  cnegex  8467  addcan  8469  addcan2  8470  negeu  8480  addsubass  8499  nppcan3  8513  muladd  8674  ltadd2  8710  add1p1  9505  div4p1lem1div2  9509  peano2z  9630  zaddcllempos  9631  zpnn0elfzo1  10575  exbtwnzlemstep  10631  rebtwn2zlemstep  10636  flhalf  10686  flqdiv  10707  binom2  11037  binom3  11043  bernneq  11047  omgadd  11191  ccatass  11321  cvg1nlemres  11695  recvguniqlem  11704  resqrexlemover  11720  bdtrilem  11949  bdtri  11950  bcxmas  12200  efsep  12402  efi4p  12428  efival  12443  divalglemnqt  12631  flodddiv4  12647  gcdaddm  12705  pcadd2  13064  4sqlem11  13124  limcimolemlt  15655  tangtx  15829  binom4  15970  2lgslem3c  16094  2lgslem3d  16095  qdiff  16959