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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2143  (class class class)co 7410  ℂcc 11102   + caddc 11107

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 11169

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1105

This theorem is used by:  mul02lem2  11391  addrid  11394  2p2e4  12379  1p2e3  12387  3p2e5  12395  3p3e6  12396  4p2e6  12397  4p3e7  12398  4p4e8  12399  5p2e7  12400  5p3e8  12401  5p4e9  12402  6p2e8  12403  6p3e9  12404  7p2e9  12405  numsuc  12729  nummac  12765  numaddc  12768  6p5lem  12790  5p5e10  12791  6p4e10  12792  7p3e10  12795  8p2e10  12800  binom2i  14253  faclbnd4lem1  14334  3dvdsdec  16394  3dvds2dec  16395  gcdaddmlem  16586  mod2xnegi  17135  decsplit  17146  lgsdir2lem2  27499  2lgsoddprmlem3d  27586  ax5seglem7  29294  normlem3  31473  stadd3i  32609  dfdec100  33183  dp3mul10  33226  dpmul  33241  dpmul4  33242  cos9thpiminplylem4  34184  quad3  36170  addassnni  42779  1p3e4  43054  sn-1ne2  43060  sqmid3api  43072  re1m1e0m0  43186  sn-0tie0  43253  fltnltalem  43422  unitadd  44949  sqwvfoura  46970  sqwvfourb  46971  fouriersw  46973  3exp4mod41  48396  bgoldbtbndlem1  48598  crosspdotsumi  50673