Theorem addassi 8013

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

Syntax hints:   = wceq 1364   ∈ wcel 2160  (class class class)co 5906  ℂcc 7856   + caddc 7861

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 7960

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

This theorem is referenced by:  2p2e4  9095  3p2e5  9109  3p3e6  9110  4p2e6  9111  4p3e7  9112  4p4e8  9113  5p2e7  9114  5p3e8  9115  5p4e9  9116  6p2e8  9117  6p3e9  9118  7p2e9  9119  numsuc  9447  nummac  9478  numaddc  9481  6p5lem  9503  5p5e10  9504  6p4e10  9505  7p3e10  9508  8p2e10  9513  binom2i  10693  resqrexlemover  11128  3dvdsdec  11980  3dvds2dec  11981  lgsdir2lem2  15073  2lgsoddprmlem3d  15122