Theorem addassi 8334

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

This proof depends on syntax axioms:   = wceq 1402   ∈ wcel 2209  (class class class)co 6085  ℂcc 8177   + caddc 8182

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-addass 8281

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  2p2e4  9431  3p2e5  9446  3p3e6  9447  4p2e6  9448  4p3e7  9449  4p4e8  9450  5p2e7  9451  5p3e8  9452  5p4e9  9453  6p2e8  9454  6p3e9  9455  7p2e9  9456  numsuc  9790  nummac  9821  numaddc  9824  6p5lem  9846  5p5e10  9847  6p4e10  9848  7p3e10  9851  8p2e10  9856  binom2i  11085  resqrexlemover  11776  3dvdsdec  12632  3dvds2dec  12633  decsplit  13208  lgsdir2lem2  16148  2lgsoddprmlem3d  16229