Theorem addassd 8355

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 8316	. 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 6088  ℂcc 8184   + caddc 8189

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 8288

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

This theorem is used by:  readdcan  8474  muladd11r  8490  cnegexlem1  8509  cnegex  8512  addcan  8514  addcan2  8515  negeu  8525  addsubass  8544  nppcan3  8558  muladd  8719  ltadd2  8755  add1p1  9567  div4p1lem1div2  9571  peano2z  9692  zaddcllempos  9693  zpnn0elfzo1  10644  exbtwnzlemstep  10700  rebtwn2zlemstep  10705  flhalf  10759  flqdiv  10780  binom2  11110  binom3  11116  bernneq  11120  omgadd  11265  ccatass  11399  cvg1nlemres  11774  recvguniqlem  11783  resqrexlemover  11799  bdtrilem  12031  bdtri  12032  bcxmas  12282  efsep  12484  efi4p  12510  efival  12525  divalglemnqt  12713  flodddiv4  12729  gcdaddm  12787  pcadd2  13150  4sqlem11  13210  limcimolemlt  15902  tangtx  16077  logfac  16138  binom4  16231  ppiqub  16305  bcp1ctr  16318  bposlem9  16331  2lgslem3c  16431  2lgslem3d  16432  qdiff  17317