Theorem adddid 8068

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167  (class class class)co 5925  ℂcc 7894   + caddc 7899   · cmul 7901

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 8000

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

This theorem is referenced by:  subdi  8428  mulreim  8648  apadd1  8652  conjmulap  8773  cju  9005  flhalf  10409  modqcyc  10468  addmodlteq  10507  binom2  10760  binom3  10766  sqoddm1div8  10802  bcpasc  10875  remim  11042  mulreap  11046  readd  11051  remullem  11053  imadd  11059  cjadd  11066  bdtrilem  11421  fsummulc2  11630  binomlem  11665  tanval3ap  11896  sinadd  11918  tanaddap  11921  bezoutlemnewy  12188  dvdsmulgcd  12217  lcmgcdlem  12270  pythagtriplem1  12459  pcaddlem  12533  mul4sqlem  12587  tangtx  15158  rpmulcxp  15229  rpcxpmul2  15233  binom4  15299  lgseisenlem2  15396  2lgsoddprmlem2  15431  2sqlem4  15443  2sqlem8  15448