Theorem addassd 8312

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2205  (class class class)co 6058  ℂcc 8141   + caddc 8146

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 8245

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

This theorem is referenced by:  readdcan  8430  muladd11r  8446  cnegexlem1  8465  cnegex  8468  addcan  8470  addcan2  8471  negeu  8481  addsubass  8500  nppcan3  8514  muladd  8675  ltadd2  8711  add1p1  9508  div4p1lem1div2  9512  peano2z  9633  zaddcllempos  9634  zpnn0elfzo1  10578  exbtwnzlemstep  10634  rebtwn2zlemstep  10639  flhalf  10689  flqdiv  10710  binom2  11040  binom3  11046  bernneq  11050  omgadd  11194  ccatass  11324  cvg1nlemres  11698  recvguniqlem  11707  resqrexlemover  11723  bdtrilem  11952  bdtri  11953  bcxmas  12203  efsep  12405  efi4p  12431  efival  12446  divalglemnqt  12634  flodddiv4  12650  gcdaddm  12708  pcadd2  13067  4sqlem11  13127  limcimolemlt  15658  tangtx  15832  binom4  15973  2lgslem3c  16097  2lgslem3d  16098  qdiff  16972