Theorem addassi 11194

Description: Associative law for addition. (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ
axi.2	⊢ 𝐵 ∈ ℂ
axi.3	⊢ 𝐶 ∈ ℂ

Assertion

Ref	Expression
addassi	⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))

Proof of Theorem addassi

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		axi.2	. 2 ⊢ 𝐵 ∈ ℂ
3		axi.3	. 2 ⊢ 𝐶 ∈ ℂ
4		addass 11162	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
5	1, 2, 3, 4	mp3an 1484	1 ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))

Syntax hints:   = wceq 1562   ∈ wcel 2144  (class class class)co 7398  ℂcc 11073   + caddc 11078

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1101

This theorem is referenced by:  mul02lem2  11362  addrid  11365  2p2e4  12354  1p2e3  12362  3p2e5  12370  3p3e6  12371  4p2e6  12372  4p3e7  12373  4p4e8  12374  5p2e7  12375  5p3e8  12376  5p4e9  12377  6p2e8  12378  6p3e9  12379  7p2e9  12380  numsuc  12704  nummac  12740  numaddc  12743  6p5lem  12765  5p5e10  12766  6p4e10  12767  7p3e10  12770  8p2e10  12775  binom2i  14227  faclbnd4lem1  14308  3dvdsdec  16368  3dvds2dec  16369  gcdaddmlem  16560  mod2xnegi  17109  decsplit  17120  lgsdir2lem2  27392  2lgsoddprmlem3d  27479  ax5seglem7  29138  normlem3  31317  stadd3i  32453  dfdec100  33034  dp3mul10  33077  dpmul  33092  dpmul4  33093  cos9thpiminplylem4  34084  quad3  36025  addassnni  42606  1p3e4  42879  sn-1ne2  42885  sqmid3api  42897  re1m1e0m0  43011  sn-0tie0  43078  fltnltalem  43249  unitadd  44776  sqwvfoura  46807  sqwvfourb  46808  fouriersw  46810  3exp4mod41  48230  bgoldbtbndlem1  48432