Theorem adddid 7981

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  (class class class)co 5874  ℂcc 7808   + caddc 7813   · cmul 7815

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 7914

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

This theorem is referenced by:  subdi  8341  mulreim  8560  apadd1  8564  conjmulap  8685  cju  8917  flhalf  10301  modqcyc  10358  addmodlteq  10397  binom2  10631  binom3  10637  sqoddm1div8  10673  bcpasc  10745  remim  10868  mulreap  10872  readd  10877  remullem  10879  imadd  10885  cjadd  10892  bdtrilem  11246  fsummulc2  11455  binomlem  11490  tanval3ap  11721  sinadd  11743  tanaddap  11746  bezoutlemnewy  11996  dvdsmulgcd  12025  lcmgcdlem  12076  pythagtriplem1  12264  pcaddlem  12337  mul4sqlem  12390  tangtx  14229  rpmulcxp  14300  binom4  14367  lgseisenlem2  14421  2lgsoddprmlem2  14424  2sqlem4  14435  2sqlem8  14440