Theorem addassi 7035

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

Syntax hints:   = wceq 1243   ∈ wcel 1393  (class class class)co 5512  ℂcc 6887   + caddc 6892

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-addass 6986

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  2p2e4  8037  3p2e5  8052  3p3e6  8053  4p2e6  8054  4p3e7  8055  4p4e8  8056  5p2e7  8057  5p3e8  8058  5p4e9  8059  5p5e10  8060  6p2e8  8061  6p3e9  8062  6p4e10  8063  7p2e9  8064  7p3e10  8065  8p2e10  8066  numsuc  8379  nummac  8399  numaddc  8402  6p5lem  8416  binom2i  9360  resqrexlemover  9608