Theorem addassd 8292

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2203  (class class class)co 6049  ℂcc 8121   + caddc 8126

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 8225

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

This theorem is referenced by:  readdcan  8409  muladd11r  8425  cnegexlem1  8444  cnegex  8447  addcan  8449  addcan2  8450  negeu  8460  addsubass  8479  nppcan3  8493  muladd  8653  ltadd2  8689  add1p1  9484  div4p1lem1div2  9488  peano2z  9609  zaddcllempos  9610  zpnn0elfzo1  10549  exbtwnzlemstep  10603  rebtwn2zlemstep  10608  flhalf  10658  flqdiv  10679  binom2  11009  binom3  11015  bernneq  11018  omgadd  11161  ccatass  11289  cvg1nlemres  11663  recvguniqlem  11672  resqrexlemover  11688  bdtrilem  11917  bdtri  11918  bcxmas  12168  efsep  12370  efi4p  12396  efival  12411  divalglemnqt  12599  flodddiv4  12615  gcdaddm  12673  pcadd2  13032  4sqlem11  13092  limcimolemlt  15516  tangtx  15690  binom4  15831  2lgslem3c  15955  2lgslem3d  15956  qdiff  16820