Theorem addassd 8190

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

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200  (class class class)co 6011   CCcc 8018   + caddc 8023

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 8122

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

This theorem is referenced by:  readdcan  8307  muladd11r  8323  cnegexlem1  8342  cnegex  8345  addcan  8347  addcan2  8348  negeu  8358  addsubass  8377  nppcan3  8391  muladd  8551  ltadd2  8587  add1p1  9382  div4p1lem1div2  9386  peano2z  9503  zaddcllempos  9504  zpnn0elfzo1  10441  exbtwnzlemstep  10495  rebtwn2zlemstep  10500  flhalf  10550  flqdiv  10571  binom2  10901  binom3  10907  bernneq  10910  omgadd  11052  ccatass  11172  cvg1nlemres  11533  recvguniqlem  11542  resqrexlemover  11558  bdtrilem  11787  bdtri  11788  bcxmas  12037  efsep  12239  efi4p  12265  efival  12280  divalglemnqt  12468  flodddiv4  12484  gcdaddm  12542  pcadd2  12901  4sqlem11  12961  limcimolemlt  15375  tangtx  15549  binom4  15690  2lgslem3c  15811  2lgslem3d  15812