Theorem addassd 8301

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2205  (class class class)co 6052  ℂcc 8130   + caddc 8135

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 8234

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

This theorem is referenced by:  readdcan  8418  muladd11r  8434  cnegexlem1  8453  cnegex  8456  addcan  8458  addcan2  8459  negeu  8469  addsubass  8488  nppcan3  8502  muladd  8662  ltadd2  8698  add1p1  9493  div4p1lem1div2  9497  peano2z  9618  zaddcllempos  9619  zpnn0elfzo1  10560  exbtwnzlemstep  10614  rebtwn2zlemstep  10619  flhalf  10669  flqdiv  10690  binom2  11020  binom3  11026  bernneq  11030  omgadd  11174  ccatass  11304  cvg1nlemres  11678  recvguniqlem  11687  resqrexlemover  11703  bdtrilem  11932  bdtri  11933  bcxmas  12183  efsep  12385  efi4p  12411  efival  12426  divalglemnqt  12614  flodddiv4  12630  gcdaddm  12688  pcadd2  13047  4sqlem11  13107  limcimolemlt  15578  tangtx  15752  binom4  15893  2lgslem3c  16017  2lgslem3d  16018  qdiff  16882