Theorem adddid 8314

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2205  (class class class)co 6058  ℂcc 8141   + caddc 8146   · cmul 8148

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 8247

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

This theorem is referenced by:  subdi  8676  mulreim  8896  apadd1  8900  conjmulap  9023  cju  9255  flhalf  10689  modqcyc  10748  addmodlteq  10787  binom2  11040  binom3  11046  sqoddm1div8  11083  bcpasc  11156  remim  11573  mulreap  11577  readd  11582  remullem  11584  imadd  11590  cjadd  11597  bdtrilem  11953  fsummulc2  12163  binomlem  12198  tanval3ap  12429  sinadd  12451  tanaddap  12454  bezoutlemnewy  12721  dvdsmulgcd  12750  lcmgcdlem  12803  pythagtriplem1  12992  pcaddlem  13066  mul4sqlem  13120  tangtx  15833  rpmulcxp  15904  rpcxpmul2  15908  binom4  15974  lgseisenlem2  16074  2lgsoddprmlem2  16109  2sqlem4  16121  2sqlem8  16126