Theorem adddid 7976

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  (class class class)co 5870  ℂcc 7804   + caddc 7809   · cmul 7811

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-distr 7910

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

This theorem is referenced by:  subdi  8336  mulreim  8555  apadd1  8559  conjmulap  8680  cju  8912  flhalf  10295  modqcyc  10352  addmodlteq  10391  binom2  10624  binom3  10630  sqoddm1div8  10666  bcpasc  10737  remim  10860  mulreap  10864  readd  10869  remullem  10871  imadd  10877  cjadd  10884  bdtrilem  11238  fsummulc2  11447  binomlem  11482  tanval3ap  11713  sinadd  11735  tanaddap  11738  bezoutlemnewy  11987  dvdsmulgcd  12016  lcmgcdlem  12067  pythagtriplem1  12255  pcaddlem  12328  mul4sqlem  12381  tangtx  14041  rpmulcxp  14112  binom4  14179  2sqlem4  14236  2sqlem8  14241