Theorem adddid 8197

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6013  ℂcc 8023   + caddc 8028   · cmul 8030

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 8129

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

This theorem is referenced by:  subdi  8557  mulreim  8777  apadd1  8781  conjmulap  8902  cju  9134  flhalf  10555  modqcyc  10614  addmodlteq  10653  binom2  10906  binom3  10912  sqoddm1div8  10948  bcpasc  11021  remim  11414  mulreap  11418  readd  11423  remullem  11425  imadd  11431  cjadd  11438  bdtrilem  11793  fsummulc2  12002  binomlem  12037  tanval3ap  12268  sinadd  12290  tanaddap  12293  bezoutlemnewy  12560  dvdsmulgcd  12589  lcmgcdlem  12642  pythagtriplem1  12831  pcaddlem  12905  mul4sqlem  12959  tangtx  15555  rpmulcxp  15626  rpcxpmul2  15630  binom4  15696  lgseisenlem2  15793  2lgsoddprmlem2  15828  2sqlem4  15840  2sqlem8  15845