Theorem addassd 8349

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6085  ℂcc 8178   + caddc 8183

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-addass 8282

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  readdcan  8468  muladd11r  8484  cnegexlem1  8503  cnegex  8506  addcan  8508  addcan2  8509  negeu  8519  addsubass  8538  nppcan3  8552  muladd  8713  ltadd2  8749  add1p1  9560  div4p1lem1div2  9564  peano2z  9685  zaddcllempos  9686  zpnn0elfzo1  10637  exbtwnzlemstep  10693  rebtwn2zlemstep  10698  flhalf  10751  flqdiv  10772  binom2  11102  binom3  11108  bernneq  11112  omgadd  11257  ccatass  11391  cvg1nlemres  11766  recvguniqlem  11775  resqrexlemover  11791  bdtrilem  12023  bdtri  12024  bcxmas  12274  efsep  12476  efi4p  12502  efival  12517  divalglemnqt  12705  flodddiv4  12721  gcdaddm  12779  pcadd2  13142  4sqlem11  13202  limcimolemlt  15817  tangtx  15992  logfac  16051  binom4  16141  ppiqub  16215  bcp1ctr  16228  2lgslem3c  16336  2lgslem3d  16337  qdiff  17220