Theorem addassi 11254

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

Syntax hints:   = wceq 1533   ∈ wcel 2098  (class class class)co 7417  ℂcc 11136   + caddc 11141

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086

This theorem is referenced by:  mul02lem2  11421  addrid  11424  2p2e4  12377  1p2e3  12385  3p2e5  12393  3p3e6  12394  4p2e6  12395  4p3e7  12396  4p4e8  12397  5p2e7  12398  5p3e8  12399  5p4e9  12400  6p2e8  12401  6p3e9  12402  7p2e9  12403  numsuc  12721  nummac  12752  numaddc  12755  6p5lem  12777  5p5e10  12778  6p4e10  12779  7p3e10  12782  8p2e10  12787  binom2i  14207  faclbnd4lem1  14284  3dvdsdec  16308  3dvds2dec  16309  gcdaddmlem  16498  mod2xnegi  17039  decexp2  17043  decsplit  17051  lgsdir2lem2  27289  2lgsoddprmlem3d  27376  ax5seglem7  28802  normlem3  30978  stadd3i  32114  dfdec100  32650  dp3mul10  32678  dpmul  32693  dpmul4  32694  quad3  35344  addassnni  41524  sn-1ne2  41905  sqmid3api  41922  re1m1e0m0  42017  sn-0tie0  42059  fltnltalem  42151  unitadd  43690  sqwvfoura  45679  sqwvfourb  45680  fouriersw  45682  3exp4mod41  47019  bgoldbtbndlem1  47208