Theorem addassd 7980

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  (class class class)co 5875  ℂcc 7809   + caddc 7814

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 7913

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

This theorem is referenced by:  readdcan  8097  muladd11r  8113  cnegexlem1  8132  cnegex  8135  addcan  8137  addcan2  8138  negeu  8148  addsubass  8167  nppcan3  8181  muladd  8341  ltadd2  8376  add1p1  9168  div4p1lem1div2  9172  peano2z  9289  zaddcllempos  9290  zpnn0elfzo1  10208  exbtwnzlemstep  10248  rebtwn2zlemstep  10253  flhalf  10302  flqdiv  10321  binom2  10632  binom3  10638  bernneq  10641  omgadd  10782  cvg1nlemres  10994  recvguniqlem  11003  resqrexlemover  11019  bdtrilem  11247  bdtri  11248  bcxmas  11497  efsep  11699  efi4p  11725  efival  11740  divalglemnqt  11925  flodddiv4  11939  gcdaddm  11985  limcimolemlt  14136  tangtx  14262  binom4  14400