Theorem adddid 8187

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6010  ℂcc 8013   + caddc 8018   · cmul 8020

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 8119

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

This theorem is referenced by:  subdi  8547  mulreim  8767  apadd1  8771  conjmulap  8892  cju  9124  flhalf  10539  modqcyc  10598  addmodlteq  10637  binom2  10890  binom3  10896  sqoddm1div8  10932  bcpasc  11005  remim  11392  mulreap  11396  readd  11401  remullem  11403  imadd  11409  cjadd  11416  bdtrilem  11771  fsummulc2  11980  binomlem  12015  tanval3ap  12246  sinadd  12268  tanaddap  12271  bezoutlemnewy  12538  dvdsmulgcd  12567  lcmgcdlem  12620  pythagtriplem1  12809  pcaddlem  12883  mul4sqlem  12937  tangtx  15533  rpmulcxp  15604  rpcxpmul2  15608  binom4  15674  lgseisenlem2  15771  2lgsoddprmlem2  15806  2sqlem4  15818  2sqlem8  15823