Theorem addassd 7979

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

Syntax hints:   -> wi 4   = wceq 1353   e. wcel 2148  (class class class)co 5874   CCcc 7808   + caddc 7813

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 7912

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

This theorem is referenced by:  readdcan  8096  muladd11r  8112  cnegexlem1  8131  cnegex  8134  addcan  8136  addcan2  8137  negeu  8147  addsubass  8166  nppcan3  8180  muladd  8340  ltadd2  8375  add1p1  9167  div4p1lem1div2  9171  peano2z  9288  zaddcllempos  9289  zpnn0elfzo1  10207  exbtwnzlemstep  10247  rebtwn2zlemstep  10252  flhalf  10301  flqdiv  10320  binom2  10631  binom3  10637  bernneq  10640  omgadd  10781  cvg1nlemres  10993  recvguniqlem  11002  resqrexlemover  11018  bdtrilem  11246  bdtri  11247  bcxmas  11496  efsep  11698  efi4p  11724  efival  11739  divalglemnqt  11924  flodddiv4  11938  gcdaddm  11984  limcimolemlt  14103  tangtx  14229  binom4  14367