Theorem addassi 8281

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

Syntax hints:   = wceq 1398   e. wcel 2203  (class class class)co 6049   CCcc 8124   + caddc 8129

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 8228

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

This theorem is referenced by:  2p2e4  9363  3p2e5  9378  3p3e6  9379  4p2e6  9380  4p3e7  9381  4p4e8  9382  5p2e7  9383  5p3e8  9384  5p4e9  9385  6p2e8  9386  6p3e9  9387  7p2e9  9388  numsuc  9721  nummac  9752  numaddc  9755  6p5lem  9777  5p5e10  9778  6p4e10  9779  7p3e10  9782  8p2e10  9787  binom2i  11009  resqrexlemover  11691  3dvdsdec  12547  3dvds2dec  12548  decsplit  13123  lgsdir2lem2  15894  2lgsoddprmlem3d  15975