Theorem addassi 7907

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 7883	. 2 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
5	1, 2, 3, 4	mp3an 1327	1 |- ( ( A + B ) + C ) = ( A + ( B + C ) )

Syntax hints:   = wceq 1343   e. wcel 2136  (class class class)co 5842   CCcc 7751   + caddc 7756

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

This theorem depends on definitions:  df-bi 116  df-3an 970

This theorem is referenced by:  2p2e4  8984  3p2e5  8998  3p3e6  8999  4p2e6  9000  4p3e7  9001  4p4e8  9002  5p2e7  9003  5p3e8  9004  5p4e9  9005  6p2e8  9006  6p3e9  9007  7p2e9  9008  numsuc  9335  nummac  9366  numaddc  9369  6p5lem  9391  5p5e10  9392  6p4e10  9393  7p3e10  9396  8p2e10  9401  binom2i  10563  resqrexlemover  10952  3dvdsdec  11802  3dvds2dec  11803  lgsdir2lem2  13570