Theorem addassd 8011

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2160  (class class class)co 5897  ℂcc 7840   + caddc 7845

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 7944

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

This theorem is referenced by:  readdcan  8128  muladd11r  8144  cnegexlem1  8163  cnegex  8166  addcan  8168  addcan2  8169  negeu  8179  addsubass  8198  nppcan3  8212  muladd  8372  ltadd2  8407  add1p1  9199  div4p1lem1div2  9203  peano2z  9320  zaddcllempos  9321  zpnn0elfzo1  10240  exbtwnzlemstep  10280  rebtwn2zlemstep  10285  flhalf  10335  flqdiv  10354  binom2  10666  binom3  10672  bernneq  10675  omgadd  10817  cvg1nlemres  11029  recvguniqlem  11038  resqrexlemover  11054  bdtrilem  11282  bdtri  11283  bcxmas  11532  efsep  11734  efi4p  11760  efival  11775  divalglemnqt  11960  flodddiv4  11974  gcdaddm  12020  pcadd2  12376  4sqlem11  12436  limcimolemlt  14610  tangtx  14736  binom4  14874