Theorem addassd 7781

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

Syntax hints:   -> wi 4   = wceq 1331   e. wcel 1480  (class class class)co 5767   CCcc 7611   + caddc 7616

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 7715

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

This theorem is referenced by:  readdcan  7895  muladd11r  7911  cnegexlem1  7930  cnegex  7933  addcan  7935  addcan2  7936  negeu  7946  addsubass  7965  nppcan3  7979  muladd  8139  ltadd2  8174  add1p1  8962  div4p1lem1div2  8966  peano2z  9083  zaddcllempos  9084  zpnn0elfzo1  9978  exbtwnzlemstep  10018  rebtwn2zlemstep  10023  flhalf  10068  flqdiv  10087  binom2  10396  binom3  10402  bernneq  10405  omgadd  10541  cvg1nlemres  10750  recvguniqlem  10759  resqrexlemover  10775  bdtrilem  11003  bdtri  11004  bcxmas  11251  efsep  11386  efi4p  11413  efival  11428  divalglemnqt  11606  flodddiv4  11620  gcdaddm  11661  limcimolemlt  12791  tangtx  12908