Theorem addassd 7788

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

Syntax hints:   → wi 4   = wceq 1331   ∈ wcel 1480  (class class class)co 5774  ℂcc 7618   + caddc 7623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-addass 7722

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  readdcan  7902  muladd11r  7918  cnegexlem1  7937  cnegex  7940  addcan  7942  addcan2  7943  negeu  7953  addsubass  7972  nppcan3  7986  muladd  8146  ltadd2  8181  add1p1  8969  div4p1lem1div2  8973  peano2z  9090  zaddcllempos  9091  zpnn0elfzo1  9985  exbtwnzlemstep  10025  rebtwn2zlemstep  10030  flhalf  10075  flqdiv  10094  binom2  10403  binom3  10409  bernneq  10412  omgadd  10548  cvg1nlemres  10757  recvguniqlem  10766  resqrexlemover  10782  bdtrilem  11010  bdtri  11011  bcxmas  11258  efsep  11397  efi4p  11424  efival  11439  divalglemnqt  11617  flodddiv4  11631  gcdaddm  11672  limcimolemlt  12802  tangtx  12919