Theorem addassd 8068

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167  (class class class)co 5925  ℂcc 7896   + caddc 7901

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 8000

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

This theorem is referenced by:  readdcan  8185  muladd11r  8201  cnegexlem1  8220  cnegex  8223  addcan  8225  addcan2  8226  negeu  8236  addsubass  8255  nppcan3  8269  muladd  8429  ltadd2  8465  add1p1  9260  div4p1lem1div2  9264  peano2z  9381  zaddcllempos  9382  zpnn0elfzo1  10303  exbtwnzlemstep  10356  rebtwn2zlemstep  10361  flhalf  10411  flqdiv  10432  binom2  10762  binom3  10768  bernneq  10771  omgadd  10913  cvg1nlemres  11169  recvguniqlem  11178  resqrexlemover  11194  bdtrilem  11423  bdtri  11424  bcxmas  11673  efsep  11875  efi4p  11901  efival  11916  divalglemnqt  12104  flodddiv4  12120  gcdaddm  12178  pcadd2  12537  4sqlem11  12597  limcimolemlt  14986  tangtx  15160  binom4  15301  2lgslem3c  15422  2lgslem3d  15423