Theorem addassi 8282

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

Syntax hints:   = wceq 1398   ∈ wcel 2203  (class class class)co 6050  ℂcc 8125   + caddc 8130

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 8229

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

This theorem is referenced by:  2p2e4  9364  3p2e5  9379  3p3e6  9380  4p2e6  9381  4p3e7  9382  4p4e8  9383  5p2e7  9384  5p3e8  9385  5p4e9  9386  6p2e8  9387  6p3e9  9388  7p2e9  9389  numsuc  9722  nummac  9753  numaddc  9756  6p5lem  9778  5p5e10  9779  6p4e10  9780  7p3e10  9783  8p2e10  9788  binom2i  11010  resqrexlemover  11695  3dvdsdec  12551  3dvds2dec  12552  decsplit  13127  lgsdir2lem2  15902  2lgsoddprmlem3d  15983