Theorem addassd 8342

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 8303	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
5	1, 2, 3, 4	syl3anc 1278	1 ⊢ (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6079  ℂcc 8171   + caddc 8176

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 8275

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

This theorem is referenced by:  readdcan  8460  muladd11r  8476  cnegexlem1  8495  cnegex  8498  addcan  8500  addcan2  8501  negeu  8511  addsubass  8530  nppcan3  8544  muladd  8705  ltadd2  8741  add1p1  9538  div4p1lem1div2  9542  peano2z  9663  zaddcllempos  9664  zpnn0elfzo1  10609  exbtwnzlemstep  10665  rebtwn2zlemstep  10670  flhalf  10720  flqdiv  10741  binom2  11071  binom3  11077  bernneq  11081  omgadd  11225  ccatass  11359  cvg1nlemres  11734  recvguniqlem  11743  resqrexlemover  11759  bdtrilem  11988  bdtri  11989  bcxmas  12239  efsep  12441  efi4p  12467  efival  12482  divalglemnqt  12670  flodddiv4  12686  gcdaddm  12744  pcadd2  13103  4sqlem11  13163  limcimolemlt  15748  tangtx  15922  logfac  15978  binom4  16064  2lgslem3c  16197  2lgslem3d  16198  qdiff  17072