Theorem addassi 8162

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 8137	. 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 6007   CCcc 8005   + caddc 8010

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 8109

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

This theorem is referenced by:  2p2e4  9245  3p2e5  9260  3p3e6  9261  4p2e6  9262  4p3e7  9263  4p4e8  9264  5p2e7  9265  5p3e8  9266  5p4e9  9267  6p2e8  9268  6p3e9  9269  7p2e9  9270  numsuc  9599  nummac  9630  numaddc  9633  6p5lem  9655  5p5e10  9656  6p4e10  9657  7p3e10  9660  8p2e10  9665  binom2i  10878  resqrexlemover  11531  3dvdsdec  12386  3dvds2dec  12387  decsplit  12962  lgsdir2lem2  15718  2lgsoddprmlem3d  15799