Theorem addassd 7203

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

Syntax hints:   -> wi 4   = wceq 1285   e. wcel 1434  (class class class)co 5543   CCcc 7041   + caddc 7046

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 7140

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

This theorem is referenced by:  readdcan  7315  muladd11r  7331  cnegexlem1  7350  cnegex  7353  addcan  7355  addcan2  7356  negeu  7366  addsubass  7385  nppcan3  7399  muladd  7555  ltadd2  7590  add1p1  8347  div4p1lem1div2  8351  peano2z  8468  zaddcllempos  8469  zpnn0elfzo1  9294  exbtwnzlemstep  9334  rebtwn2zlemstep  9339  flhalf  9384  flqdiv  9403  binom2  9682  binom3  9687  bernneq  9690  omgadd  9826  cvg1nlemres  10009  recvguniqlem  10018  resqrexlemover  10034  divalglemnqt  10464  flodddiv4  10478  gcdaddm  10519