Theorem addassi 7127

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

Syntax hints:   = wceq 1284   e. wcel 1433  (class class class)co 5532   CCcc 6979   + caddc 6984

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

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  2p2e4  8159  3p2e5  8173  3p3e6  8174  4p2e6  8175  4p3e7  8176  4p4e8  8177  5p2e7  8178  5p3e8  8179  5p4e9  8180  6p2e8  8181  6p3e9  8182  7p2e9  8183  numsuc  8490  nummac  8521  numaddc  8524  6p5lem  8546  5p5e10  8547  6p4e10  8548  7p3e10  8551  8p2e10  8556  binom2i  9583  resqrexlemover  9896  3dvdsdec  10264  3dvds2dec  10265