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  8675  mulreim  8895  apadd1  8899  conjmulap  9020  cju  9252  flhalf  10686  modqcyc  10745  addmodlteq  10784  binom2  11037  binom3  11043  sqoddm1div8  11080  bcpasc  11153  remim  11570  mulreap  11574  readd  11579  remullem  11581  imadd  11587  cjadd  11594  bdtrilem  11949  fsummulc2  12159  binomlem  12194  tanval3ap  12425  sinadd  12447  tanaddap  12450  bezoutlemnewy  12717  dvdsmulgcd  12746  lcmgcdlem  12799  pythagtriplem1  12988  pcaddlem  13062  mul4sqlem  13116  tangtx  15815  rpmulcxp  15886  rpcxpmul2  15890  binom4  15956  lgseisenlem2  16056  2lgsoddprmlem2  16091  2sqlem4  16103  2sqlem8  16108