Theorem addassd 7976

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

Syntax hints:   -> wi 4   = wceq 1353   e. wcel 2148  (class class class)co 5872   CCcc 7806   + caddc 7811

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 7910

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

This theorem is referenced by:  readdcan  8093  muladd11r  8109  cnegexlem1  8128  cnegex  8131  addcan  8133  addcan2  8134  negeu  8144  addsubass  8163  nppcan3  8177  muladd  8337  ltadd2  8372  add1p1  9164  div4p1lem1div2  9168  peano2z  9285  zaddcllempos  9286  zpnn0elfzo1  10203  exbtwnzlemstep  10243  rebtwn2zlemstep  10248  flhalf  10297  flqdiv  10316  binom2  10626  binom3  10632  bernneq  10635  omgadd  10775  cvg1nlemres  10987  recvguniqlem  10996  resqrexlemover  11012  bdtrilem  11240  bdtri  11241  bcxmas  11490  efsep  11692  efi4p  11718  efival  11733  divalglemnqt  11917  flodddiv4  11931  gcdaddm  11977  limcimolemlt  14004  tangtx  14130  binom4  14268