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  10758  modqcyc  10817  addmodlteq  10856  binom2  11109  binom3  11115  sqoddm1div8  11152  bcpasc  11226  hashf1lem2  11308  remim  11647  mulreap  11651  readd  11656  remullem  11658  imadd  11664  cjadd  11671  bdtrilem  12030  fsummulc2  12240  binomlem  12275  tanval3ap  12506  sinadd  12528  tanaddap  12531  bezoutlemnewy  12798  dvdsmulgcd  12827  lcmgcdlem  12880  pythagtriplem1  13073  pcaddlem  13147  mul4sqlem  13201  tangtx  16098  rpmulcxp  16175  rpcxpmul2  16179  binom4  16252  chtqub  16329  bposlem9  16352  lgseisenlem2  16428  2lgsoddprmlem2  16463  2sqlem4  16475  2sqlem8  16480