Theorem addassi 7928

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

Syntax hints:   = wceq 1348   e. wcel 2141  (class class class)co 5853   CCcc 7772   + caddc 7777

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 7876

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

This theorem is referenced by:  2p2e4  9005  3p2e5  9019  3p3e6  9020  4p2e6  9021  4p3e7  9022  4p4e8  9023  5p2e7  9024  5p3e8  9025  5p4e9  9026  6p2e8  9027  6p3e9  9028  7p2e9  9029  numsuc  9356  nummac  9387  numaddc  9390  6p5lem  9412  5p5e10  9413  6p4e10  9414  7p3e10  9417  8p2e10  9422  binom2i  10584  resqrexlemover  10974  3dvdsdec  11824  3dvds2dec  11825  lgsdir2lem2  13724