Theorem adddid 7790

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

Syntax hints:   → wi 4   = wceq 1331   ∈ wcel 1480  (class class class)co 5774  ℂcc 7618   + caddc 7623   · cmul 7625

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 7724

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

This theorem is referenced by:  subdi  8147  mulreim  8366  apadd1  8370  conjmulap  8489  cju  8719  flhalf  10075  modqcyc  10132  addmodlteq  10171  binom2  10403  binom3  10409  sqoddm1div8  10444  bcpasc  10512  remim  10632  mulreap  10636  readd  10641  remullem  10643  imadd  10649  cjadd  10656  bdtrilem  11010  fsummulc2  11217  binomlem  11252  tanval3ap  11421  sinadd  11443  tanaddap  11446  bezoutlemnewy  11684  dvdsmulgcd  11713  lcmgcdlem  11758  tangtx  12919