Theorem addassd 7489

Description: Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
addassd.3	⊢ (𝜑 → 𝐶 ∈ ℂ)

Assertion

Ref	Expression
addassd	⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Proof of Theorem addassd

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addassd.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		addass 7451	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
5	1, 2, 3, 4	syl3anc 1174	1 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Syntax hints:   → wi 4   = wceq 1289   ∈ wcel 1438  (class class class)co 5634  ℂcc 7327   + caddc 7332

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-addass 7426

This theorem depends on definitions:  df-bi 115  df-3an 926

This theorem is referenced by:  readdcan  7601  muladd11r  7617  cnegexlem1  7636  cnegex  7639  addcan  7641  addcan2  7642  negeu  7652  addsubass  7671  nppcan3  7685  muladd  7841  ltadd2  7876  add1p1  8635  div4p1lem1div2  8639  peano2z  8756  zaddcllempos  8757  zpnn0elfzo1  9584  exbtwnzlemstep  9624  rebtwn2zlemstep  9629  flhalf  9674  flqdiv  9693  binom2  10030  binom3  10036  bernneq  10039  omgadd  10175  cvg1nlemres  10383  recvguniqlem  10392  resqrexlemover  10408  bcxmas  10845  divalglemnqt  11013  flodddiv4  11027  gcdaddm  11068