Theorem addassd 7967

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  (class class class)co 5869  ℂcc 7797   + caddc 7802

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 7901

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

This theorem is referenced by:  readdcan  8084  muladd11r  8100  cnegexlem1  8119  cnegex  8122  addcan  8124  addcan2  8125  negeu  8135  addsubass  8154  nppcan3  8168  muladd  8328  ltadd2  8363  add1p1  9154  div4p1lem1div2  9158  peano2z  9275  zaddcllempos  9276  zpnn0elfzo1  10191  exbtwnzlemstep  10231  rebtwn2zlemstep  10236  flhalf  10285  flqdiv  10304  binom2  10614  binom3  10620  bernneq  10623  omgadd  10763  cvg1nlemres  10975  recvguniqlem  10984  resqrexlemover  11000  bdtrilem  11228  bdtri  11229  bcxmas  11478  efsep  11680  efi4p  11706  efival  11721  divalglemnqt  11905  flodddiv4  11919  gcdaddm  11965  limcimolemlt  13793  tangtx  13919  binom4  14057