Theorem addassi 11223

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

Syntax hints:   = wceq 1541   ∈ wcel 2106  (class class class)co 7408  ℂcc 11107   + caddc 11112

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1089

This theorem is referenced by:  mul02lem2  11390  addrid  11393  2p2e4  12346  1p2e3  12354  3p2e5  12362  3p3e6  12363  4p2e6  12364  4p3e7  12365  4p4e8  12366  5p2e7  12367  5p3e8  12368  5p4e9  12369  6p2e8  12370  6p3e9  12371  7p2e9  12372  numsuc  12690  nummac  12721  numaddc  12724  6p5lem  12746  5p5e10  12747  6p4e10  12748  7p3e10  12751  8p2e10  12756  binom2i  14175  faclbnd4lem1  14252  3dvdsdec  16274  3dvds2dec  16275  gcdaddmlem  16464  mod2xnegi  17003  decexp2  17007  decsplit  17015  lgsdir2lem2  26826  2lgsoddprmlem3d  26913  ax5seglem7  28190  normlem3  30360  stadd3i  31496  dfdec100  32031  dp3mul10  32059  dpmul  32074  dpmul4  32075  quad3  34650  addassnni  40845  sn-1ne2  41181  sqmid3api  41197  re1m1e0m0  41271  sn-0tie0  41313  fltnltalem  41405  unitadd  42937  sqwvfoura  44934  sqwvfourb  44935  fouriersw  44937  3exp4mod41  46274  bgoldbtbndlem1  46463