Theorem addassi 8328

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

Syntax hints:   = wceq 1402   e. wcel 2209  (class class class)co 6079   CCcc 8171   + caddc 8176

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 8275

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

This theorem is referenced by:  2p2e4  9414  3p2e5  9429  3p3e6  9430  4p2e6  9431  4p3e7  9432  4p4e8  9433  5p2e7  9434  5p3e8  9435  5p4e9  9436  6p2e8  9437  6p3e9  9438  7p2e9  9439  numsuc  9773  nummac  9804  numaddc  9807  6p5lem  9829  5p5e10  9830  6p4e10  9831  7p3e10  9834  8p2e10  9839  binom2i  11068  resqrexlemover  11759  3dvdsdec  12615  3dvds2dec  12616  decsplit  13191  lgsdir2lem2  16131  2lgsoddprmlem3d  16212