Theorem adddid 7903

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

Syntax hints:   → wi 4   = wceq 1335   ∈ wcel 2128  (class class class)co 5825  ℂcc 7731   + caddc 7736   · cmul 7738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-distr 7837

This theorem depends on definitions:  df-bi 116  df-3an 965

This theorem is referenced by:  subdi  8261  mulreim  8480  apadd1  8484  conjmulap  8603  cju  8833  flhalf  10205  modqcyc  10262  addmodlteq  10301  binom2  10533  binom3  10539  sqoddm1div8  10575  bcpasc  10644  remim  10764  mulreap  10768  readd  10773  remullem  10775  imadd  10781  cjadd  10788  bdtrilem  11142  fsummulc2  11349  binomlem  11384  tanval3ap  11615  sinadd  11637  tanaddap  11640  bezoutlemnewy  11884  dvdsmulgcd  11913  lcmgcdlem  11958  pythagtriplem1  12144  tangtx  13201  rpmulcxp  13272  binom4  13338