Theorem addassi 7967

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

Syntax hints:   = wceq 1353   e. wcel 2148  (class class class)co 5877   CCcc 7811   + caddc 7816

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 7915

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

This theorem is referenced by:  2p2e4  9048  3p2e5  9062  3p3e6  9063  4p2e6  9064  4p3e7  9065  4p4e8  9066  5p2e7  9067  5p3e8  9068  5p4e9  9069  6p2e8  9070  6p3e9  9071  7p2e9  9072  numsuc  9399  nummac  9430  numaddc  9433  6p5lem  9455  5p5e10  9456  6p4e10  9457  7p3e10  9460  8p2e10  9465  binom2i  10631  resqrexlemover  11021  3dvdsdec  11872  3dvds2dec  11873  lgsdir2lem2  14515  2lgsoddprmlem3d  14543