Theorem addassi 11253

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

Syntax hints:   = wceq 1539   ∈ wcel 2107  (class class class)co 7413  ℂcc 11135   + caddc 11140

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

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

This theorem is referenced by:  mul02lem2  11420  addrid  11423  2p2e4  12383  1p2e3  12391  3p2e5  12399  3p3e6  12400  4p2e6  12401  4p3e7  12402  4p4e8  12403  5p2e7  12404  5p3e8  12405  5p4e9  12406  6p2e8  12407  6p3e9  12408  7p2e9  12409  numsuc  12730  nummac  12761  numaddc  12764  6p5lem  12786  5p5e10  12787  6p4e10  12788  7p3e10  12791  8p2e10  12796  binom2i  14233  faclbnd4lem1  14314  3dvdsdec  16351  3dvds2dec  16352  gcdaddmlem  16543  mod2xnegi  17091  decsplit  17102  lgsdir2lem2  27306  2lgsoddprmlem3d  27393  ax5seglem7  28880  normlem3  31059  stadd3i  32195  dfdec100  32772  dp3mul10  32820  dpmul  32835  dpmul4  32836  quad3  35634  addassnni  41944  sn-1ne2  42263  sqmid3api  42281  re1m1e0m0  42390  sn-0tie0  42432  fltnltalem  42635  unitadd  44170  sqwvfoura  46200  sqwvfourb  46201  fouriersw  46203  3exp4mod41  47561  bgoldbtbndlem1  47750