Theorem addassd 7974

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 7936	. 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 5870   CCcc 7804   + caddc 7809

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 7908

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

This theorem is referenced by:  readdcan  8091  muladd11r  8107  cnegexlem1  8126  cnegex  8129  addcan  8131  addcan2  8132  negeu  8142  addsubass  8161  nppcan3  8175  muladd  8335  ltadd2  8370  add1p1  9162  div4p1lem1div2  9166  peano2z  9283  zaddcllempos  9284  zpnn0elfzo1  10201  exbtwnzlemstep  10241  rebtwn2zlemstep  10246  flhalf  10295  flqdiv  10314  binom2  10624  binom3  10630  bernneq  10633  omgadd  10773  cvg1nlemres  10985  recvguniqlem  10994  resqrexlemover  11010  bdtrilem  11238  bdtri  11239  bcxmas  11488  efsep  11690  efi4p  11716  efival  11731  divalglemnqt  11915  flodddiv4  11929  gcdaddm  11975  limcimolemlt  13915  tangtx  14041  binom4  14179