Theorem addassd 8296

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 8257	. 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 2203  (class class class)co 6050   CCcc 8125   + caddc 8130

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 8229

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

This theorem is referenced by:  readdcan  8413  muladd11r  8429  cnegexlem1  8448  cnegex  8451  addcan  8453  addcan2  8454  negeu  8464  addsubass  8483  nppcan3  8497  muladd  8657  ltadd2  8693  add1p1  9488  div4p1lem1div2  9492  peano2z  9613  zaddcllempos  9614  zpnn0elfzo1  10553  exbtwnzlemstep  10607  rebtwn2zlemstep  10612  flhalf  10662  flqdiv  10683  binom2  11013  binom3  11019  bernneq  11022  omgadd  11166  ccatass  11296  cvg1nlemres  11670  recvguniqlem  11679  resqrexlemover  11695  bdtrilem  11924  bdtri  11925  bcxmas  12175  efsep  12377  efi4p  12403  efival  12418  divalglemnqt  12606  flodddiv4  12622  gcdaddm  12680  pcadd2  13039  4sqlem11  13099  limcimolemlt  15529  tangtx  15703  binom4  15844  2lgslem3c  15968  2lgslem3d  15969  qdiff  16833