Theorem adddid 8056

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167  (class class class)co 5925  ℂcc 7882   + caddc 7887   · cmul 7889

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 7988

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

This theorem is referenced by:  subdi  8416  mulreim  8636  apadd1  8640  conjmulap  8761  cju  8993  flhalf  10397  modqcyc  10456  addmodlteq  10495  binom2  10748  binom3  10754  sqoddm1div8  10790  bcpasc  10863  remim  11030  mulreap  11034  readd  11039  remullem  11041  imadd  11047  cjadd  11054  bdtrilem  11409  fsummulc2  11618  binomlem  11653  tanval3ap  11884  sinadd  11906  tanaddap  11909  bezoutlemnewy  12176  dvdsmulgcd  12205  lcmgcdlem  12258  pythagtriplem1  12447  pcaddlem  12521  mul4sqlem  12575  tangtx  15121  rpmulcxp  15192  rpcxpmul2  15196  binom4  15262  lgseisenlem2  15359  2lgsoddprmlem2  15394  2sqlem4  15406  2sqlem8  15411