Theorem addassi 8150

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

Syntax hints:   = wceq 1395   ∈ wcel 2200  (class class class)co 6000  ℂcc 7993   + caddc 7998

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 8097

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

This theorem is referenced by:  2p2e4  9233  3p2e5  9248  3p3e6  9249  4p2e6  9250  4p3e7  9251  4p4e8  9252  5p2e7  9253  5p3e8  9254  5p4e9  9255  6p2e8  9256  6p3e9  9257  7p2e9  9258  numsuc  9587  nummac  9618  numaddc  9621  6p5lem  9643  5p5e10  9644  6p4e10  9645  7p3e10  9648  8p2e10  9653  binom2i  10865  resqrexlemover  11516  3dvdsdec  12371  3dvds2dec  12372  decsplit  12947  lgsdir2lem2  15702  2lgsoddprmlem3d  15783