Theorem addassi 10985

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

Syntax hints:   = wceq 1539   ∈ wcel 2106  (class class class)co 7275  ℂcc 10869   + caddc 10874

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

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

This theorem is referenced by:  mul02lem2  11152  addid1  11155  2p2e4  12108  1p2e3  12116  3p2e5  12124  3p3e6  12125  4p2e6  12126  4p3e7  12127  4p4e8  12128  5p2e7  12129  5p3e8  12130  5p4e9  12131  6p2e8  12132  6p3e9  12133  7p2e9  12134  numsuc  12451  nummac  12482  numaddc  12485  6p5lem  12507  5p5e10  12508  6p4e10  12509  7p3e10  12512  8p2e10  12517  binom2i  13928  faclbnd4lem1  14007  3dvdsdec  16041  3dvds2dec  16042  gcdaddmlem  16231  mod2xnegi  16772  decexp2  16776  decsplit  16784  lgsdir2lem2  26474  2lgsoddprmlem3d  26561  ax5seglem7  27303  normlem3  29474  stadd3i  30610  dfdec100  31144  dp3mul10  31172  dpmul  31187  dpmul4  31188  quad3  33628  addassnni  39993  sn-1ne2  40295  sqmid3api  40311  re1m1e0m0  40380  sn-0tie0  40421  fltnltalem  40499  unitadd  41806  sqwvfoura  43769  sqwvfourb  43770  fouriersw  43772  3exp4mod41  45068  bgoldbtbndlem1  45257