Theorem addassi 7978

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

Syntax hints:   = wceq 1363   ∈ wcel 2158  (class class class)co 5888  ℂcc 7822   + caddc 7827

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 7926

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

This theorem is referenced by:  2p2e4  9059  3p2e5  9073  3p3e6  9074  4p2e6  9075  4p3e7  9076  4p4e8  9077  5p2e7  9078  5p3e8  9079  5p4e9  9080  6p2e8  9081  6p3e9  9082  7p2e9  9083  numsuc  9410  nummac  9441  numaddc  9444  6p5lem  9466  5p5e10  9467  6p4e10  9468  7p3e10  9471  8p2e10  9476  binom2i  10642  resqrexlemover  11032  3dvdsdec  11883  3dvds2dec  11884  lgsdir2lem2  14701  2lgsoddprmlem3d  14729