Theorem addassi 7888

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

Syntax hints:   = wceq 1335   e. wcel 2128  (class class class)co 5826   CCcc 7732   + caddc 7737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-addass 7836

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  2p2e4  8965  3p2e5  8979  3p3e6  8980  4p2e6  8981  4p3e7  8982  4p4e8  8983  5p2e7  8984  5p3e8  8985  5p4e9  8986  6p2e8  8987  6p3e9  8988  7p2e9  8989  numsuc  9313  nummac  9344  numaddc  9347  6p5lem  9369  5p5e10  9370  6p4e10  9371  7p3e10  9374  8p2e10  9379  binom2i  10536  resqrexlemover  10921  3dvdsdec  11768  3dvds2dec  11769