Theorem addassd 8137

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

Syntax hints:   → wi 4   = wceq 1375   ∈ wcel 2180  (class class class)co 5974  ℂcc 7965   + caddc 7970

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 8069

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

This theorem is referenced by:  readdcan  8254  muladd11r  8270  cnegexlem1  8289  cnegex  8292  addcan  8294  addcan2  8295  negeu  8305  addsubass  8324  nppcan3  8338  muladd  8498  ltadd2  8534  add1p1  9329  div4p1lem1div2  9333  peano2z  9450  zaddcllempos  9451  zpnn0elfzo1  10381  exbtwnzlemstep  10434  rebtwn2zlemstep  10439  flhalf  10489  flqdiv  10510  binom2  10840  binom3  10846  bernneq  10849  omgadd  10991  ccatass  11109  cvg1nlemres  11462  recvguniqlem  11471  resqrexlemover  11487  bdtrilem  11716  bdtri  11717  bcxmas  11966  efsep  12168  efi4p  12194  efival  12209  divalglemnqt  12397  flodddiv4  12413  gcdaddm  12471  pcadd2  12830  4sqlem11  12890  limcimolemlt  15303  tangtx  15477  binom4  15618  2lgslem3c  15739  2lgslem3d  15740