Theorem addassi 8335

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

This proof depends on syntax axioms:   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 8178   + caddc 8183

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-addass 8282

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  2p2e4  9434  3p2e5  9449  3p3e6  9450  4p2e6  9451  4p3e7  9452  4p4e8  9453  5p2e7  9454  5p3e8  9455  5p4e9  9456  6p2e8  9457  6p3e9  9458  7p2e9  9459  numsuc  9795  nummac  9831  numaddc  9834  6p5lem  9856  5p5e10  9857  6p4e10  9858  7p3e10  9861  8p2e10  9866  binom2i  11099  resqrexlemover  11791  3dvdsdec  12650  3dvds2dec  12651  mod2xnegi  13220  decsplit  13231  lgsdir2lem2  16270  2lgsoddprmlem3d  16351