Theorem addassd 8348

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6085  ℂcc 8177   + caddc 8182

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-addass 8281

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

This theorem is used by:  readdcan  8466  muladd11r  8482  cnegexlem1  8501  cnegex  8504  addcan  8506  addcan2  8507  negeu  8517  addsubass  8536  nppcan3  8550  muladd  8711  ltadd2  8747  add1p1  9557  div4p1lem1div2  9561  peano2z  9682  zaddcllempos  9683  zpnn0elfzo1  10628  exbtwnzlemstep  10684  rebtwn2zlemstep  10689  flhalf  10739  flqdiv  10760  binom2  11090  binom3  11096  bernneq  11100  omgadd  11244  ccatass  11378  cvg1nlemres  11753  recvguniqlem  11762  resqrexlemover  11778  bdtrilem  12007  bdtri  12008  bcxmas  12258  efsep  12460  efi4p  12486  efival  12501  divalglemnqt  12689  flodddiv4  12705  gcdaddm  12763  pcadd2  13122  4sqlem11  13182  limcimolemlt  15767  tangtx  15942  logfac  16001  binom4  16087  bcp1ctr  16126  2lgslem3c  16226  2lgslem3d  16227  qdiff  17110