Theorem addassi 8298

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 8273	. 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 6058   CCcc 8141   + caddc 8146

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 8245

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

This theorem is referenced by:  2p2e4  9381  3p2e5  9396  3p3e6  9397  4p2e6  9398  4p3e7  9399  4p4e8  9400  5p2e7  9401  5p3e8  9402  5p4e9  9403  6p2e8  9404  6p3e9  9405  7p2e9  9406  numsuc  9740  nummac  9771  numaddc  9774  6p5lem  9796  5p5e10  9797  6p4e10  9798  7p3e10  9801  8p2e10  9806  binom2i  11034  resqrexlemover  11720  3dvdsdec  12576  3dvds2dec  12577  decsplit  13152  lgsdir2lem2  16014  2lgsoddprmlem3d  16095