Theorem addassi 7798

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

Syntax hints:   = wceq 1332   ∈ wcel 1481  (class class class)co 5782  ℂcc 7642   + caddc 7647

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

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  2p2e4  8871  3p2e5  8885  3p3e6  8886  4p2e6  8887  4p3e7  8888  4p4e8  8889  5p2e7  8890  5p3e8  8891  5p4e9  8892  6p2e8  8893  6p3e9  8894  7p2e9  8895  numsuc  9219  nummac  9250  numaddc  9253  6p5lem  9275  5p5e10  9276  6p4e10  9277  7p3e10  9280  8p2e10  9285  binom2i  10432  resqrexlemover  10814  3dvdsdec  11598  3dvds2dec  11599