Theorem addassi 8027

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 8002	. 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 2164  (class class class)co 5918   CCcc 7870   + caddc 7875

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 7974

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

This theorem is referenced by:  2p2e4  9109  3p2e5  9123  3p3e6  9124  4p2e6  9125  4p3e7  9126  4p4e8  9127  5p2e7  9128  5p3e8  9129  5p4e9  9130  6p2e8  9131  6p3e9  9132  7p2e9  9133  numsuc  9461  nummac  9492  numaddc  9495  6p5lem  9517  5p5e10  9518  6p4e10  9519  7p3e10  9522  8p2e10  9527  binom2i  10719  resqrexlemover  11154  3dvdsdec  12006  3dvds2dec  12007  lgsdir2lem2  15145  2lgsoddprmlem3d  15198