Theorem addassi 8187

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

Syntax hints:   = wceq 1397   e. wcel 2202  (class class class)co 6018   CCcc 8030   + caddc 8035

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 8134

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

This theorem is referenced by:  2p2e4  9270  3p2e5  9285  3p3e6  9286  4p2e6  9287  4p3e7  9288  4p4e8  9289  5p2e7  9290  5p3e8  9291  5p4e9  9292  6p2e8  9293  6p3e9  9294  7p2e9  9295  numsuc  9624  nummac  9655  numaddc  9658  6p5lem  9680  5p5e10  9681  6p4e10  9682  7p3e10  9685  8p2e10  9690  binom2i  10911  resqrexlemover  11575  3dvdsdec  12431  3dvds2dec  12432  decsplit  13007  lgsdir2lem2  15764  2lgsoddprmlem3d  15845