Theorem addassi 8170

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 8145	. 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 6010   CCcc 8013   + caddc 8018

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 8117

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

This theorem is referenced by:  2p2e4  9253  3p2e5  9268  3p3e6  9269  4p2e6  9270  4p3e7  9271  4p4e8  9272  5p2e7  9273  5p3e8  9274  5p4e9  9275  6p2e8  9276  6p3e9  9277  7p2e9  9278  numsuc  9607  nummac  9638  numaddc  9641  6p5lem  9663  5p5e10  9664  6p4e10  9665  7p3e10  9668  8p2e10  9673  binom2i  10887  resqrexlemover  11542  3dvdsdec  12397  3dvds2dec  12398  decsplit  12973  lgsdir2lem2  15729  2lgsoddprmlem3d  15810