Theorem addassi 8299

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

Syntax hints:   = wceq 1398   e. wcel 2205  (class class class)co 6059   CCcc 8142   + caddc 8147

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 8246

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

This theorem is referenced by:  2p2e4  9385  3p2e5  9400  3p3e6  9401  4p2e6  9402  4p3e7  9403  4p4e8  9404  5p2e7  9405  5p3e8  9406  5p4e9  9407  6p2e8  9408  6p3e9  9409  7p2e9  9410  numsuc  9744  nummac  9775  numaddc  9778  6p5lem  9800  5p5e10  9801  6p4e10  9802  7p3e10  9805  8p2e10  9810  binom2i  11038  resqrexlemover  11725  3dvdsdec  12581  3dvds2dec  12582  decsplit  13157  lgsdir2lem2  16033  2lgsoddprmlem3d  16114