Theorem addassi 8051

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

Syntax hints:   = wceq 1364   e. wcel 2167  (class class class)co 5925   CCcc 7894   + caddc 7899

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 7998

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

This theorem is referenced by:  2p2e4  9134  3p2e5  9149  3p3e6  9150  4p2e6  9151  4p3e7  9152  4p4e8  9153  5p2e7  9154  5p3e8  9155  5p4e9  9156  6p2e8  9157  6p3e9  9158  7p2e9  9159  numsuc  9487  nummac  9518  numaddc  9521  6p5lem  9543  5p5e10  9544  6p4e10  9545  7p3e10  9548  8p2e10  9553  binom2i  10757  resqrexlemover  11192  3dvdsdec  12047  3dvds2dec  12048  decsplit  12623  lgsdir2lem2  15354  2lgsoddprmlem3d  15435