Theorem addassi 8034

Description: Associative law for addition. (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	|- A e. CC
axi.2	|- B e. CC
axi.3	|- C e. CC

Assertion

Ref	Expression
addassi	|- ( ( A + B ) + C ) = ( A + ( B + C ) )

Proof of Theorem addassi

Step	Hyp	Ref	Expression
1		axi.1	. 2 |- A e. CC
2		axi.2	. 2 |- B e. CC
3		axi.3	. 2 |- C e. CC
4		addass 8009	. 2 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
5	1, 2, 3, 4	mp3an 1348	1 |- ( ( A + B ) + C ) = ( A + ( B + C ) )

Syntax hints:   = wceq 1364   e. wcel 2167  (class class class)co 5922   CCcc 7877   + caddc 7882

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 7981

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

This theorem is referenced by:  2p2e4  9117  3p2e5  9132  3p3e6  9133  4p2e6  9134  4p3e7  9135  4p4e8  9136  5p2e7  9137  5p3e8  9138  5p4e9  9139  6p2e8  9140  6p3e9  9141  7p2e9  9142  numsuc  9470  nummac  9501  numaddc  9504  6p5lem  9526  5p5e10  9527  6p4e10  9528  7p3e10  9531  8p2e10  9536  binom2i  10740  resqrexlemover  11175  3dvdsdec  12030  3dvds2dec  12031  decsplit  12598  lgsdir2lem2  15270  2lgsoddprmlem3d  15351