Theorem addassd 8169

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6001  ℂcc 7997   + caddc 8002

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 8101

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

This theorem is referenced by:  readdcan  8286  muladd11r  8302  cnegexlem1  8321  cnegex  8324  addcan  8326  addcan2  8327  negeu  8337  addsubass  8356  nppcan3  8370  muladd  8530  ltadd2  8566  add1p1  9361  div4p1lem1div2  9365  peano2z  9482  zaddcllempos  9483  zpnn0elfzo1  10414  exbtwnzlemstep  10467  rebtwn2zlemstep  10472  flhalf  10522  flqdiv  10543  binom2  10873  binom3  10879  bernneq  10882  omgadd  11024  ccatass  11143  cvg1nlemres  11496  recvguniqlem  11505  resqrexlemover  11521  bdtrilem  11750  bdtri  11751  bcxmas  12000  efsep  12202  efi4p  12228  efival  12243  divalglemnqt  12431  flodddiv4  12447  gcdaddm  12505  pcadd2  12864  4sqlem11  12924  limcimolemlt  15338  tangtx  15512  binom4  15653  2lgslem3c  15774  2lgslem3d  15775