Theorem addassd 7902

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

Syntax hints:   -> wi 4   = wceq 1335   e. wcel 2128  (class class class)co 5826   CCcc 7732   + caddc 7737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-addass 7836

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  readdcan  8019  muladd11r  8035  cnegexlem1  8054  cnegex  8057  addcan  8059  addcan2  8060  negeu  8070  addsubass  8089  nppcan3  8103  muladd  8263  ltadd2  8298  add1p1  9087  div4p1lem1div2  9091  peano2z  9208  zaddcllempos  9209  zpnn0elfzo1  10116  exbtwnzlemstep  10156  rebtwn2zlemstep  10161  flhalf  10210  flqdiv  10229  binom2  10538  binom3  10544  bernneq  10547  omgadd  10687  cvg1nlemres  10896  recvguniqlem  10905  resqrexlemover  10921  bdtrilem  11149  bdtri  11150  bcxmas  11397  efsep  11599  efi4p  11625  efival  11640  divalglemnqt  11823  flodddiv4  11837  gcdaddm  11883  limcimolemlt  13103  tangtx  13229  binom4  13367