Theorem addassi 8341

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 8316	. 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 6088   CCcc 8184   + caddc 8189

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 8288

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

This theorem is used by:  2p2e4  9441  3p2e5  9456  3p3e6  9457  4p2e6  9458  4p3e7  9459  4p4e8  9460  5p2e7  9461  5p3e8  9462  5p4e9  9463  6p2e8  9464  6p3e9  9465  7p2e9  9466  numsuc  9801  nummac  9837  numaddc  9840  6p5lem  9862  5p5e10  9863  6p4e10  9864  7p3e10  9867  8p2e10  9872  binom2i  11106  resqrexlemover  11798  3dvdsdec  12657  3dvds2dec  12658  mod2xnegi  13227  decsplit  13238  lgsdir2lem2  16386  2lgsoddprmlem3d  16467