Theorem addassd 7812

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

Syntax hints:   -> wi 4   = wceq 1332   e. wcel 1481  (class class class)co 5782   CCcc 7642   + caddc 7647

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 7746

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

This theorem is referenced by:  readdcan  7926  muladd11r  7942  cnegexlem1  7961  cnegex  7964  addcan  7966  addcan2  7967  negeu  7977  addsubass  7996  nppcan3  8010  muladd  8170  ltadd2  8205  add1p1  8993  div4p1lem1div2  8997  peano2z  9114  zaddcllempos  9115  zpnn0elfzo1  10016  exbtwnzlemstep  10056  rebtwn2zlemstep  10061  flhalf  10106  flqdiv  10125  binom2  10434  binom3  10440  bernneq  10443  omgadd  10580  cvg1nlemres  10789  recvguniqlem  10798  resqrexlemover  10814  bdtrilem  11042  bdtri  11043  bcxmas  11290  efsep  11434  efi4p  11460  efival  11475  divalglemnqt  11653  flodddiv4  11667  gcdaddm  11708  limcimolemlt  12841  tangtx  12967