Theorem adddid 8344

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

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209  (class class class)co 6079  ℂcc 8171   + caddc 8176   · cmul 8178

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 8277

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

This theorem is referenced by:  subdi  8706  mulreim  8926  apadd1  8930  conjmulap  9053  cju  9285  flhalf  10720  modqcyc  10779  addmodlteq  10818  binom2  11071  binom3  11077  sqoddm1div8  11114  bcpasc  11187  hashf1lem2  11269  remim  11608  mulreap  11612  readd  11617  remullem  11619  imadd  11625  cjadd  11632  bdtrilem  11988  fsummulc2  12198  binomlem  12233  tanval3ap  12464  sinadd  12486  tanaddap  12489  bezoutlemnewy  12756  dvdsmulgcd  12785  lcmgcdlem  12838  pythagtriplem1  13027  pcaddlem  13101  mul4sqlem  13155  tangtx  15922  rpmulcxp  15994  rpcxpmul2  15998  binom4  16064  lgseisenlem2  16173  2lgsoddprmlem2  16208  2sqlem4  16220  2sqlem8  16225