Theorem addassi 11150

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

Syntax hints:   = wceq 1548   ∈ wcel 2121  (class class class)co 7360  ℂcc 11031   + caddc 11036

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

This theorem depends on definitions:  df-bi 209  df-an 398  df-3an 1095

This theorem is referenced by:  mul02lem2  11318  addrid  11321  2p2e4  12306  1p2e3  12314  3p2e5  12322  3p3e6  12323  4p2e6  12324  4p3e7  12325  4p4e8  12326  5p2e7  12327  5p3e8  12328  5p4e9  12329  6p2e8  12330  6p3e9  12331  7p2e9  12332  numsuc  12653  nummac  12684  numaddc  12687  6p5lem  12709  5p5e10  12710  6p4e10  12711  7p3e10  12714  8p2e10  12719  binom2i  14169  faclbnd4lem1  14250  3dvdsdec  16296  3dvds2dec  16297  gcdaddmlem  16488  mod2xnegi  17037  decsplit  17048  lgsdir2lem2  27311  2lgsoddprmlem3d  27398  ax5seglem7  29026  normlem3  31205  stadd3i  32341  dfdec100  32926  dp3mul10  32980  dpmul  32995  dpmul4  32996  cos9thpiminplylem4  33981  quad3  35913  addassnni  42484  1p3e4  42757  sn-1ne2  42763  sqmid3api  42775  re1m1e0m0  42889  sn-0tie0  42956  fltnltalem  43127  unitadd  44654  sqwvfoura  46685  sqwvfourb  46686  fouriersw  46688  3exp4mod41  48108  bgoldbtbndlem1  48310