Theorem addassi 11302

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

Syntax hints:   = wceq 1537   ∈ wcel 2108  (class class class)co 7450  ℂcc 11184   + caddc 11189

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

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

This theorem is referenced by:  mul02lem2  11469  addrid  11472  2p2e4  12430  1p2e3  12438  3p2e5  12446  3p3e6  12447  4p2e6  12448  4p3e7  12449  4p4e8  12450  5p2e7  12451  5p3e8  12452  5p4e9  12453  6p2e8  12454  6p3e9  12455  7p2e9  12456  numsuc  12774  nummac  12805  numaddc  12808  6p5lem  12830  5p5e10  12831  6p4e10  12832  7p3e10  12835  8p2e10  12840  binom2i  14263  faclbnd4lem1  14344  3dvdsdec  16382  3dvds2dec  16383  gcdaddmlem  16572  mod2xnegi  17120  decexp2  17124  decsplit  17132  lgsdir2lem2  27390  2lgsoddprmlem3d  27477  ax5seglem7  28970  normlem3  31146  stadd3i  32282  dfdec100  32836  dp3mul10  32864  dpmul  32879  dpmul4  32880  quad3  35640  addassnni  41943  sn-1ne2  42256  sqmid3api  42274  re1m1e0m0  42375  sn-0tie0  42417  fltnltalem  42619  unitadd  44159  sqwvfoura  46151  sqwvfourb  46152  fouriersw  46154  3exp4mod41  47492  bgoldbtbndlem1  47681