Theorem addassi 10048

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

Syntax hints:   = wceq 1483   e. wcel 1990  (class class class)co 6650   CCcc 9934   + caddc 9939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 10001

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  mul02lem2  10213  addid1  10216  2p2e4  11144  3p2e5  11160  3p3e6  11161  4p2e6  11162  4p3e7  11163  4p4e8  11164  5p2e7  11165  5p3e8  11166  5p4e9  11167  5p5e10OLD  11168  6p2e8  11169  6p3e9  11170  6p4e10OLD  11171  7p2e9  11172  7p3e10OLD  11173  8p2e10OLD  11174  numsuc  11511  nummac  11558  numaddc  11561  6p5lem  11595  5p5e10  11596  6p4e10  11598  7p3e10  11603  8p2e10  11610  binom2i  12974  faclbnd4lem1  13080  3dvdsdec  15054  3dvdsdecOLD  15055  3dvds2dec  15056  3dvds2decOLD  15057  gcdaddmlem  15245  mod2xnegi  15775  decexp2  15779  decsplit  15787  decsplitOLD  15791  lgsdir2lem2  25051  2lgsoddprmlem3d  25138  ax5seglem7  25815  normlem3  27969  stadd3i  29107  dfdec100  29576  dp3mul10  29606  dpmul  29621  dpmul4  29622  quad3  31564  unitadd  38498  sqwvfoura  40445  sqwvfourb  40446  fouriersw  40448  3exp4mod41  41533  bgoldbtbndlem1  41693