Theorem addassd 7942

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

Syntax hints:   -> wi 4   = wceq 1348   e. wcel 2141  (class class class)co 5853   CCcc 7772   + caddc 7777

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 7876

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

This theorem is referenced by:  readdcan  8059  muladd11r  8075  cnegexlem1  8094  cnegex  8097  addcan  8099  addcan2  8100  negeu  8110  addsubass  8129  nppcan3  8143  muladd  8303  ltadd2  8338  add1p1  9127  div4p1lem1div2  9131  peano2z  9248  zaddcllempos  9249  zpnn0elfzo1  10164  exbtwnzlemstep  10204  rebtwn2zlemstep  10209  flhalf  10258  flqdiv  10277  binom2  10587  binom3  10593  bernneq  10596  omgadd  10737  cvg1nlemres  10949  recvguniqlem  10958  resqrexlemover  10974  bdtrilem  11202  bdtri  11203  bcxmas  11452  efsep  11654  efi4p  11680  efival  11695  divalglemnqt  11879  flodddiv4  11893  gcdaddm  11939  limcimolemlt  13427  tangtx  13553  binom4  13691