Theorem addassi 8180

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

Syntax hints:   = wceq 1395   e. wcel 2200  (class class class)co 6013   CCcc 8023   + caddc 8028

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 8127

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

This theorem is referenced by:  2p2e4  9263  3p2e5  9278  3p3e6  9279  4p2e6  9280  4p3e7  9281  4p4e8  9282  5p2e7  9283  5p3e8  9284  5p4e9  9285  6p2e8  9286  6p3e9  9287  7p2e9  9288  numsuc  9617  nummac  9648  numaddc  9651  6p5lem  9673  5p5e10  9674  6p4e10  9675  7p3e10  9678  8p2e10  9683  binom2i  10903  resqrexlemover  11564  3dvdsdec  12419  3dvds2dec  12420  decsplit  12995  lgsdir2lem2  15751  2lgsoddprmlem3d  15832