Theorem addassd 8185

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6010  ℂcc 8013   + caddc 8018

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 8117

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

This theorem is referenced by:  readdcan  8302  muladd11r  8318  cnegexlem1  8337  cnegex  8340  addcan  8342  addcan2  8343  negeu  8353  addsubass  8372  nppcan3  8386  muladd  8546  ltadd2  8582  add1p1  9377  div4p1lem1div2  9381  peano2z  9498  zaddcllempos  9499  zpnn0elfzo1  10431  exbtwnzlemstep  10484  rebtwn2zlemstep  10489  flhalf  10539  flqdiv  10560  binom2  10890  binom3  10896  bernneq  10899  omgadd  11041  ccatass  11161  cvg1nlemres  11517  recvguniqlem  11526  resqrexlemover  11542  bdtrilem  11771  bdtri  11772  bcxmas  12021  efsep  12223  efi4p  12249  efival  12264  divalglemnqt  12452  flodddiv4  12468  gcdaddm  12526  pcadd2  12885  4sqlem11  12945  limcimolemlt  15359  tangtx  15533  binom4  15674  2lgslem3c  15795  2lgslem3d  15796