Theorem adddid 7985

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  (class class class)co 5878  ℂcc 7812   + caddc 7817   · cmul 7819

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 7918

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

This theorem is referenced by:  subdi  8345  mulreim  8564  apadd1  8568  conjmulap  8689  cju  8921  flhalf  10305  modqcyc  10362  addmodlteq  10401  binom2  10635  binom3  10641  sqoddm1div8  10677  bcpasc  10749  remim  10872  mulreap  10876  readd  10881  remullem  10883  imadd  10889  cjadd  10896  bdtrilem  11250  fsummulc2  11459  binomlem  11494  tanval3ap  11725  sinadd  11747  tanaddap  11750  bezoutlemnewy  12000  dvdsmulgcd  12029  lcmgcdlem  12080  pythagtriplem1  12268  pcaddlem  12341  mul4sqlem  12394  tangtx  14420  rpmulcxp  14491  binom4  14558  lgseisenlem2  14612  2lgsoddprmlem2  14615  2sqlem4  14626  2sqlem8  14631