Theorem addassi 7774

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

Syntax hints:   = wceq 1331   e. wcel 1480  (class class class)co 5774   CCcc 7618   + caddc 7623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-addass 7722

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  2p2e4  8847  3p2e5  8861  3p3e6  8862  4p2e6  8863  4p3e7  8864  4p4e8  8865  5p2e7  8866  5p3e8  8867  5p4e9  8868  6p2e8  8869  6p3e9  8870  7p2e9  8871  numsuc  9195  nummac  9226  numaddc  9229  6p5lem  9251  5p5e10  9252  6p4e10  9253  7p3e10  9256  8p2e10  9261  binom2i  10401  resqrexlemover  10782  3dvdsdec  11562  3dvds2dec  11563