Theorem addassi 8093

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

Syntax hints:   = wceq 1373   e. wcel 2177  (class class class)co 5954   CCcc 7936   + caddc 7941

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 8040

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

This theorem is referenced by:  2p2e4  9176  3p2e5  9191  3p3e6  9192  4p2e6  9193  4p3e7  9194  4p4e8  9195  5p2e7  9196  5p3e8  9197  5p4e9  9198  6p2e8  9199  6p3e9  9200  7p2e9  9201  numsuc  9530  nummac  9561  numaddc  9564  6p5lem  9586  5p5e10  9587  6p4e10  9588  7p3e10  9591  8p2e10  9596  binom2i  10806  resqrexlemover  11371  3dvdsdec  12226  3dvds2dec  12227  decsplit  12802  lgsdir2lem2  15556  2lgsoddprmlem3d  15637