Theorem addassi 11122

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 11093	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
5	1, 2, 3, 4	mp3an 1463	1 ⊢ ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))

Syntax hints:   = wceq 1541   ∈ wcel 2111  (class class class)co 7346  ℂcc 11004   + caddc 11009

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  mul02lem2  11290  addrid  11293  2p2e4  12255  1p2e3  12263  3p2e5  12271  3p3e6  12272  4p2e6  12273  4p3e7  12274  4p4e8  12275  5p2e7  12276  5p3e8  12277  5p4e9  12278  6p2e8  12279  6p3e9  12280  7p2e9  12281  numsuc  12602  nummac  12633  numaddc  12636  6p5lem  12658  5p5e10  12659  6p4e10  12660  7p3e10  12663  8p2e10  12668  binom2i  14119  faclbnd4lem1  14200  3dvdsdec  16243  3dvds2dec  16244  gcdaddmlem  16435  mod2xnegi  16983  decsplit  16994  lgsdir2lem2  27264  2lgsoddprmlem3d  27351  ax5seglem7  28913  normlem3  31092  stadd3i  32228  dfdec100  32813  dp3mul10  32878  dpmul  32893  dpmul4  32894  cos9thpiminplylem4  33798  quad3  35714  addassnni  42087  1p3e4  42362  sn-1ne2  42368  sqmid3api  42386  re1m1e0m0  42500  sn-0tie0  42554  fltnltalem  42765  unitadd  44298  sqwvfoura  46336  sqwvfourb  46337  fouriersw  46339  3exp4mod41  47726  bgoldbtbndlem1  47915