Theorem adddid 8350

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6085  ℂcc 8177   + caddc 8182   · cmul 8184

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-distr 8283

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  subdi  8712  mulreim  8933  apadd1  8937  conjmulap  9060  cju  9292  flhalf  10739  modqcyc  10798  addmodlteq  10837  binom2  11090  binom3  11096  sqoddm1div8  11133  bcpasc  11206  hashf1lem2  11288  remim  11627  mulreap  11631  readd  11636  remullem  11638  imadd  11644  cjadd  11651  bdtrilem  12007  fsummulc2  12217  binomlem  12252  tanval3ap  12483  sinadd  12505  tanaddap  12508  bezoutlemnewy  12775  dvdsmulgcd  12804  lcmgcdlem  12857  pythagtriplem1  13046  pcaddlem  13120  mul4sqlem  13174  tangtx  15942  rpmulcxp  16017  rpcxpmul2  16021  binom4  16087  lgseisenlem2  16202  2lgsoddprmlem2  16237  2sqlem4  16249  2sqlem8  16254