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  9690  zaddcllempos  9691  zpnn0elfzo1  10643  exbtwnzlemstep  10699  rebtwn2zlemstep  10704  flhalf  10758  flqdiv  10779  binom2  11109  binom3  11115  bernneq  11119  omgadd  11264  ccatass  11398  cvg1nlemres  11773  recvguniqlem  11782  resqrexlemover  11798  bdtrilem  12030  bdtri  12031  bcxmas  12281  efsep  12483  efi4p  12509  efival  12524  divalglemnqt  12712  flodddiv4  12728  gcdaddm  12786  pcadd2  13149  4sqlem11  13209  limcimolemlt  15923  tangtx  16098  logfac  16159  binom4  16252  ppiqub  16326  bcp1ctr  16339  bposlem9  16352  2lgslem3c  16452  2lgslem3d  16453  qdiff  17338