Theorem addassi 7964

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

Syntax hints:   = wceq 1353   ∈ wcel 2148  (class class class)co 5874  ℂcc 7808   + caddc 7813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-addass 7912

This theorem depends on definitions:  df-bi 117  df-3an 980

This theorem is referenced by:  2p2e4  9044  3p2e5  9058  3p3e6  9059  4p2e6  9060  4p3e7  9061  4p4e8  9062  5p2e7  9063  5p3e8  9064  5p4e9  9065  6p2e8  9066  6p3e9  9067  7p2e9  9068  numsuc  9395  nummac  9426  numaddc  9429  6p5lem  9451  5p5e10  9452  6p4e10  9453  7p3e10  9456  8p2e10  9461  binom2i  10625  resqrexlemover  11014  3dvdsdec  11864  3dvds2dec  11865  lgsdir2lem2  14361