Theorem addassi 8186

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

Syntax hints:   = wceq 1397   ∈ wcel 2202  (class class class)co 6017  ℂcc 8029   + caddc 8034

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 8133

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

This theorem is referenced by:  2p2e4  9269  3p2e5  9284  3p3e6  9285  4p2e6  9286  4p3e7  9287  4p4e8  9288  5p2e7  9289  5p3e8  9290  5p4e9  9291  6p2e8  9292  6p3e9  9293  7p2e9  9294  numsuc  9623  nummac  9654  numaddc  9657  6p5lem  9679  5p5e10  9680  6p4e10  9681  7p3e10  9684  8p2e10  9689  binom2i  10909  resqrexlemover  11570  3dvdsdec  12425  3dvds2dec  12426  decsplit  13001  lgsdir2lem2  15757  2lgsoddprmlem3d  15838