Theorem addassd 7982

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 7943	. 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 5877   CCcc 7811   + caddc 7816

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 7915

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

This theorem is referenced by:  readdcan  8099  muladd11r  8115  cnegexlem1  8134  cnegex  8137  addcan  8139  addcan2  8140  negeu  8150  addsubass  8169  nppcan3  8183  muladd  8343  ltadd2  8378  add1p1  9170  div4p1lem1div2  9174  peano2z  9291  zaddcllempos  9292  zpnn0elfzo1  10210  exbtwnzlemstep  10250  rebtwn2zlemstep  10255  flhalf  10304  flqdiv  10323  binom2  10634  binom3  10640  bernneq  10643  omgadd  10784  cvg1nlemres  10996  recvguniqlem  11005  resqrexlemover  11021  bdtrilem  11249  bdtri  11250  bcxmas  11499  efsep  11701  efi4p  11727  efival  11742  divalglemnqt  11927  flodddiv4  11941  gcdaddm  11987  limcimolemlt  14172  tangtx  14298  binom4  14436