Theorem addassd 7712

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

Syntax hints:   → wi 4   = wceq 1314   ∈ wcel 1463  (class class class)co 5728  ℂcc 7545   + caddc 7550

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-addass 7647

This theorem depends on definitions:  df-bi 116  df-3an 947

This theorem is referenced by:  readdcan  7825  muladd11r  7841  cnegexlem1  7860  cnegex  7863  addcan  7865  addcan2  7866  negeu  7876  addsubass  7895  nppcan3  7909  muladd  8065  ltadd2  8100  add1p1  8873  div4p1lem1div2  8877  peano2z  8994  zaddcllempos  8995  zpnn0elfzo1  9878  exbtwnzlemstep  9918  rebtwn2zlemstep  9923  flhalf  9968  flqdiv  9987  binom2  10296  binom3  10302  bernneq  10305  omgadd  10441  cvg1nlemres  10649  recvguniqlem  10658  resqrexlemover  10674  bdtrilem  10902  bdtri  10903  bcxmas  11150  efsep  11248  efi4p  11275  efival  11290  divalglemnqt  11465  flodddiv4  11479  gcdaddm  11520  limcimolemlt  12589