Theorem addassi 7985

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 7961	. 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 2160  (class class class)co 5892   CCcc 7829   + caddc 7834

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 7933

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

This theorem is referenced by:  2p2e4  9066  3p2e5  9080  3p3e6  9081  4p2e6  9082  4p3e7  9083  4p4e8  9084  5p2e7  9085  5p3e8  9086  5p4e9  9087  6p2e8  9088  6p3e9  9089  7p2e9  9090  numsuc  9417  nummac  9448  numaddc  9451  6p5lem  9473  5p5e10  9474  6p4e10  9475  7p3e10  9478  8p2e10  9483  binom2i  10649  resqrexlemover  11039  3dvdsdec  11890  3dvds2dec  11891  lgsdir2lem2  14834  2lgsoddprmlem3d  14862