Theorem adddid 8357

Description: Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
addassd.3	⊢ (𝜑 → 𝐶 ∈ ℂ)

Assertion

Ref	Expression
adddid	⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Proof of Theorem adddid

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addassd.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		adddi 8318	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1278	1 ⊢ (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6088  ℂcc 8184   + caddc 8189   · cmul 8191

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-distr 8290

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  subdi  8720  mulreim  8941  apadd1  8945  conjmulap  9068  cju  9300  flhalf  10759  modqcyc  10818  addmodlteq  10857  binom2  11110  binom3  11116  sqoddm1div8  11153  bcpasc  11227  hashf1lem2  11309  remim  11648  mulreap  11652  readd  11657  remullem  11659  imadd  11665  cjadd  11672  bdtrilem  12031  fsummulc2  12241  binomlem  12276  tanval3ap  12507  sinadd  12529  tanaddap  12532  bezoutlemnewy  12799  dvdsmulgcd  12828  lcmgcdlem  12881  pythagtriplem1  13074  pcaddlem  13148  mul4sqlem  13202  tangtx  16077  rpmulcxp  16154  rpcxpmul2  16158  binom4  16231  chtqub  16308  bposlem9  16331  lgseisenlem2  16407  2lgsoddprmlem2  16442  2sqlem4  16454  2sqlem8  16459