Theorem addassd 8042

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

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2164  (class class class)co 5918   CCcc 7870   + caddc 7875

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 7974

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

This theorem is referenced by:  readdcan  8159  muladd11r  8175  cnegexlem1  8194  cnegex  8197  addcan  8199  addcan2  8200  negeu  8210  addsubass  8229  nppcan3  8243  muladd  8403  ltadd2  8438  add1p1  9232  div4p1lem1div2  9236  peano2z  9353  zaddcllempos  9354  zpnn0elfzo1  10275  exbtwnzlemstep  10316  rebtwn2zlemstep  10321  flhalf  10371  flqdiv  10392  binom2  10722  binom3  10728  bernneq  10731  omgadd  10873  cvg1nlemres  11129  recvguniqlem  11138  resqrexlemover  11154  bdtrilem  11382  bdtri  11383  bcxmas  11632  efsep  11834  efi4p  11860  efival  11875  divalglemnqt  12061  flodddiv4  12075  gcdaddm  12121  pcadd2  12479  4sqlem11  12539  limcimolemlt  14818  tangtx  14973  binom4  15111