Theorem addassi 8324

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

Syntax hints:   = wceq 1402   ∈ wcel 2209  (class class class)co 6075  ℂcc 8167   + caddc 8172

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 8271

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

This theorem is referenced by:  2p2e4  9410  3p2e5  9425  3p3e6  9426  4p2e6  9427  4p3e7  9428  4p4e8  9429  5p2e7  9430  5p3e8  9431  5p4e9  9432  6p2e8  9433  6p3e9  9434  7p2e9  9435  numsuc  9769  nummac  9800  numaddc  9803  6p5lem  9825  5p5e10  9826  6p4e10  9827  7p3e10  9830  8p2e10  9835  binom2i  11063  resqrexlemover  11754  3dvdsdec  12610  3dvds2dec  12611  decsplit  13186  lgsdir2lem2  16062  2lgsoddprmlem3d  16143