Theorem addassd 7141

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

Syntax hints:   -> wi 4   = wceq 1284   e. wcel 1433  (class class class)co 5532   CCcc 6979   + caddc 6984

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 7078

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

This theorem is referenced by:  readdcan  7248  muladd11r  7264  cnegexlem1  7283  cnegex  7286  addcan  7288  addcan2  7289  negeu  7299  addsubass  7318  nppcan3  7332  muladd  7488  ltadd2  7523  add1p1  8280  div4p1lem1div2  8284  peano2z  8387  zaddcllempos  8388  zpnn0elfzo1  9217  qbtwnzlemstep  9257  rebtwn2zlemstep  9261  flhalf  9304  flqdiv  9323  binom2  9585  binom3  9590  bernneq  9593  cvg1nlemres  9871  recvguniqlem  9880  resqrexlemover  9896  divalglemnqt  10320  flodddiv4  10334  gcdaddm  10375