Theorem addassd 7510

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

Syntax hints:   -> wi 4   = wceq 1289   e. wcel 1438  (class class class)co 5652   CCcc 7348   + caddc 7353

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-addass 7447

This theorem depends on definitions:  df-bi 115  df-3an 926

This theorem is referenced by:  readdcan  7622  muladd11r  7638  cnegexlem1  7657  cnegex  7660  addcan  7662  addcan2  7663  negeu  7673  addsubass  7692  nppcan3  7706  muladd  7862  ltadd2  7897  add1p1  8665  div4p1lem1div2  8669  peano2z  8786  zaddcllempos  8787  zpnn0elfzo1  9619  exbtwnzlemstep  9659  rebtwn2zlemstep  9664  flhalf  9709  flqdiv  9728  binom2  10065  binom3  10071  bernneq  10074  omgadd  10210  cvg1nlemres  10418  recvguniqlem  10427  resqrexlemover  10443  bcxmas  10883  efsep  10981  efi4p  11008  efival  11023  divalglemnqt  11198  flodddiv4  11212  gcdaddm  11253