Theorem addassi 8115

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

Syntax hints:   = wceq 1373   ∈ wcel 2178  (class class class)co 5967  ℂcc 7958   + caddc 7963

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 8062

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

This theorem is referenced by:  2p2e4  9198  3p2e5  9213  3p3e6  9214  4p2e6  9215  4p3e7  9216  4p4e8  9217  5p2e7  9218  5p3e8  9219  5p4e9  9220  6p2e8  9221  6p3e9  9222  7p2e9  9223  numsuc  9552  nummac  9583  numaddc  9586  6p5lem  9608  5p5e10  9609  6p4e10  9610  7p3e10  9613  8p2e10  9618  binom2i  10830  resqrexlemover  11436  3dvdsdec  12291  3dvds2dec  12292  decsplit  12867  lgsdir2lem2  15621  2lgsoddprmlem3d  15702