Theorem addassd 8177

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6007  ℂcc 8005   + caddc 8010

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 8109

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

This theorem is referenced by:  readdcan  8294  muladd11r  8310  cnegexlem1  8329  cnegex  8332  addcan  8334  addcan2  8335  negeu  8345  addsubass  8364  nppcan3  8378  muladd  8538  ltadd2  8574  add1p1  9369  div4p1lem1div2  9373  peano2z  9490  zaddcllempos  9491  zpnn0elfzo1  10422  exbtwnzlemstep  10475  rebtwn2zlemstep  10480  flhalf  10530  flqdiv  10551  binom2  10881  binom3  10887  bernneq  10890  omgadd  11032  ccatass  11151  cvg1nlemres  11504  recvguniqlem  11513  resqrexlemover  11529  bdtrilem  11758  bdtri  11759  bcxmas  12008  efsep  12210  efi4p  12236  efival  12251  divalglemnqt  12439  flodddiv4  12455  gcdaddm  12513  pcadd2  12872  4sqlem11  12932  limcimolemlt  15346  tangtx  15520  binom4  15661  2lgslem3c  15782  2lgslem3d  15783