Theorem addassi 8230

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

Syntax hints:   = wceq 1398   ∈ wcel 2202  (class class class)co 6028  ℂcc 8073   + caddc 8078

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 8177

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

This theorem is referenced by:  2p2e4  9312  3p2e5  9327  3p3e6  9328  4p2e6  9329  4p3e7  9330  4p4e8  9331  5p2e7  9332  5p3e8  9333  5p4e9  9334  6p2e8  9335  6p3e9  9336  7p2e9  9337  numsuc  9668  nummac  9699  numaddc  9702  6p5lem  9724  5p5e10  9725  6p4e10  9726  7p3e10  9729  8p2e10  9734  binom2i  10956  resqrexlemover  11633  3dvdsdec  12489  3dvds2dec  12490  decsplit  13065  lgsdir2lem2  15831  2lgsoddprmlem3d  15912