Theorem addassd 8195

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6013  ℂcc 8023   + caddc 8028

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 8127

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

This theorem is referenced by:  readdcan  8312  muladd11r  8328  cnegexlem1  8347  cnegex  8350  addcan  8352  addcan2  8353  negeu  8363  addsubass  8382  nppcan3  8396  muladd  8556  ltadd2  8592  add1p1  9387  div4p1lem1div2  9391  peano2z  9508  zaddcllempos  9509  zpnn0elfzo1  10446  exbtwnzlemstep  10500  rebtwn2zlemstep  10505  flhalf  10555  flqdiv  10576  binom2  10906  binom3  10912  bernneq  10915  omgadd  11058  ccatass  11178  cvg1nlemres  11539  recvguniqlem  11548  resqrexlemover  11564  bdtrilem  11793  bdtri  11794  bcxmas  12043  efsep  12245  efi4p  12271  efival  12286  divalglemnqt  12474  flodddiv4  12490  gcdaddm  12548  pcadd2  12907  4sqlem11  12967  limcimolemlt  15381  tangtx  15555  binom4  15696  2lgslem3c  15817  2lgslem3d  15818