Theorem addassd 8244

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 8205	. 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 2202  (class class class)co 6028   CCcc 8073   + caddc 8078

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 8177

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

This theorem is referenced by:  readdcan  8361  muladd11r  8377  cnegexlem1  8396  cnegex  8399  addcan  8401  addcan2  8402  negeu  8412  addsubass  8431  nppcan3  8445  muladd  8605  ltadd2  8641  add1p1  9436  div4p1lem1div2  9440  peano2z  9559  zaddcllempos  9560  zpnn0elfzo1  10499  exbtwnzlemstep  10553  rebtwn2zlemstep  10558  flhalf  10608  flqdiv  10629  binom2  10959  binom3  10965  bernneq  10968  omgadd  11111  ccatass  11234  cvg1nlemres  11608  recvguniqlem  11617  resqrexlemover  11633  bdtrilem  11862  bdtri  11863  bcxmas  12113  efsep  12315  efi4p  12341  efival  12356  divalglemnqt  12544  flodddiv4  12560  gcdaddm  12618  pcadd2  12977  4sqlem11  13037  limcimolemlt  15458  tangtx  15632  binom4  15773  2lgslem3c  15897  2lgslem3d  15898  qdiff  16764