Theorem addassi 10640

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

Syntax hints:   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524   + caddc 10529

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086

This theorem is referenced by:  mul02lem2  10806  addid1  10809  2p2e4  11760  1p2e3  11768  3p2e5  11776  3p3e6  11777  4p2e6  11778  4p3e7  11779  4p4e8  11780  5p2e7  11781  5p3e8  11782  5p4e9  11783  6p2e8  11784  6p3e9  11785  7p2e9  11786  numsuc  12100  nummac  12131  numaddc  12134  6p5lem  12156  5p5e10  12157  6p4e10  12158  7p3e10  12161  8p2e10  12166  binom2i  13570  faclbnd4lem1  13649  3dvdsdec  15673  3dvds2dec  15674  gcdaddmlem  15862  mod2xnegi  16397  decexp2  16401  decsplit  16409  lgsdir2lem2  25910  2lgsoddprmlem3d  25997  ax5seglem7  26729  normlem3  28895  stadd3i  30031  dfdec100  30572  dp3mul10  30600  dpmul  30615  dpmul4  30616  quad3  33026  addassnni  39272  sn-1ne2  39466  sqmid3api  39477  re1m1e0m0  39535  sn-0tie0  39576  fltnltalem  39618  unitadd  40901  sqwvfoura  42870  sqwvfourb  42871  fouriersw  42873  3exp4mod41  44134  bgoldbtbndlem1  44323