Theorem addassi 8177

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

Syntax hints:   = wceq 1395   ∈ wcel 2200  (class class class)co 6013  ℂcc 8020   + caddc 8025

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 8124

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

This theorem is referenced by:  2p2e4  9260  3p2e5  9275  3p3e6  9276  4p2e6  9277  4p3e7  9278  4p4e8  9279  5p2e7  9280  5p3e8  9281  5p4e9  9282  6p2e8  9283  6p3e9  9284  7p2e9  9285  numsuc  9614  nummac  9645  numaddc  9648  6p5lem  9670  5p5e10  9671  6p4e10  9672  7p3e10  9675  8p2e10  9680  binom2i  10900  resqrexlemover  11561  3dvdsdec  12416  3dvds2dec  12417  decsplit  12992  lgsdir2lem2  15748  2lgsoddprmlem3d  15829