Theorem addassd 8202

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

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202  (class class class)co 6018  ℂcc 8030   + caddc 8035

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 8134

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

This theorem is referenced by:  readdcan  8319  muladd11r  8335  cnegexlem1  8354  cnegex  8357  addcan  8359  addcan2  8360  negeu  8370  addsubass  8389  nppcan3  8403  muladd  8563  ltadd2  8599  add1p1  9394  div4p1lem1div2  9398  peano2z  9515  zaddcllempos  9516  zpnn0elfzo1  10454  exbtwnzlemstep  10508  rebtwn2zlemstep  10513  flhalf  10563  flqdiv  10584  binom2  10914  binom3  10920  bernneq  10923  omgadd  11066  ccatass  11186  cvg1nlemres  11547  recvguniqlem  11556  resqrexlemover  11572  bdtrilem  11801  bdtri  11802  bcxmas  12052  efsep  12254  efi4p  12280  efival  12295  divalglemnqt  12483  flodddiv4  12499  gcdaddm  12557  pcadd2  12916  4sqlem11  12976  limcimolemlt  15391  tangtx  15565  binom4  15706  2lgslem3c  15827  2lgslem3d  15828