Theorem addassi 7965

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 7941	. 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 5875   CCcc 7809   + caddc 7814

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 7913

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

This theorem is referenced by:  2p2e4  9046  3p2e5  9060  3p3e6  9061  4p2e6  9062  4p3e7  9063  4p4e8  9064  5p2e7  9065  5p3e8  9066  5p4e9  9067  6p2e8  9068  6p3e9  9069  7p2e9  9070  numsuc  9397  nummac  9428  numaddc  9431  6p5lem  9453  5p5e10  9454  6p4e10  9455  7p3e10  9458  8p2e10  9463  binom2i  10629  resqrexlemover  11019  3dvdsdec  11870  3dvds2dec  11871  lgsdir2lem2  14433  2lgsoddprmlem3d  14461