Theorem addassi 11190

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  (class class class)co 7389  ℂcc 11072   + caddc 11077

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

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

This theorem is referenced by:  mul02lem2  11357  addrid  11360  2p2e4  12322  1p2e3  12330  3p2e5  12338  3p3e6  12339  4p2e6  12340  4p3e7  12341  4p4e8  12342  5p2e7  12343  5p3e8  12344  5p4e9  12345  6p2e8  12346  6p3e9  12347  7p2e9  12348  numsuc  12669  nummac  12700  numaddc  12703  6p5lem  12725  5p5e10  12726  6p4e10  12727  7p3e10  12730  8p2e10  12735  binom2i  14183  faclbnd4lem1  14264  3dvdsdec  16308  3dvds2dec  16309  gcdaddmlem  16500  mod2xnegi  17048  decsplit  17059  lgsdir2lem2  27243  2lgsoddprmlem3d  27330  ax5seglem7  28868  normlem3  31047  stadd3i  32183  dfdec100  32761  dp3mul10  32824  dpmul  32839  dpmul4  32840  cos9thpiminplylem4  33781  quad3  35657  addassnni  41967  1p3e4  42242  sn-1ne2  42248  sqmid3api  42266  re1m1e0m0  42380  sn-0tie0  42434  fltnltalem  42643  unitadd  44177  sqwvfoura  46219  sqwvfourb  46220  fouriersw  46222  3exp4mod41  47607  bgoldbtbndlem1  47796