Theorem addassd 8207

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

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2201  (class class class)co 6023  ℂcc 8035   + caddc 8040

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 8139

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

This theorem is referenced by:  readdcan  8324  muladd11r  8340  cnegexlem1  8359  cnegex  8362  addcan  8364  addcan2  8365  negeu  8375  addsubass  8394  nppcan3  8408  muladd  8568  ltadd2  8604  add1p1  9399  div4p1lem1div2  9403  peano2z  9520  zaddcllempos  9521  zpnn0elfzo1  10459  exbtwnzlemstep  10513  rebtwn2zlemstep  10518  flhalf  10568  flqdiv  10589  binom2  10919  binom3  10925  bernneq  10928  omgadd  11071  ccatass  11194  cvg1nlemres  11568  recvguniqlem  11577  resqrexlemover  11593  bdtrilem  11822  bdtri  11823  bcxmas  12073  efsep  12275  efi4p  12301  efival  12316  divalglemnqt  12504  flodddiv4  12520  gcdaddm  12578  pcadd2  12937  4sqlem11  12997  limcimolemlt  15417  tangtx  15591  binom4  15732  2lgslem3c  15853  2lgslem3d  15854  qdiff  16720