Theorem addassd 8066

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 8026	. 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 1364   e. wcel 2167  (class class class)co 5925   CCcc 7894   + caddc 7899

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 7998

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

This theorem is referenced by:  readdcan  8183  muladd11r  8199  cnegexlem1  8218  cnegex  8221  addcan  8223  addcan2  8224  negeu  8234  addsubass  8253  nppcan3  8267  muladd  8427  ltadd2  8463  add1p1  9258  div4p1lem1div2  9262  peano2z  9379  zaddcllempos  9380  zpnn0elfzo1  10301  exbtwnzlemstep  10354  rebtwn2zlemstep  10359  flhalf  10409  flqdiv  10430  binom2  10760  binom3  10766  bernneq  10769  omgadd  10911  cvg1nlemres  11167  recvguniqlem  11176  resqrexlemover  11192  bdtrilem  11421  bdtri  11422  bcxmas  11671  efsep  11873  efi4p  11899  efival  11914  divalglemnqt  12102  flodddiv4  12118  gcdaddm  12176  pcadd2  12535  4sqlem11  12595  limcimolemlt  14984  tangtx  15158  binom4  15299  2lgslem3c  15420  2lgslem3d  15421