Theorem adddid 8297

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

Syntax hints:   → wi 4   = wceq 1398   ∈ wcel 2203  (class class class)co 6049  ℂcc 8124   + caddc 8129   · cmul 8131

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 8230

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

This theorem is referenced by:  subdi  8657  mulreim  8877  apadd1  8881  conjmulap  9002  cju  9234  flhalf  10661  modqcyc  10720  addmodlteq  10759  binom2  11012  binom3  11018  sqoddm1div8  11054  bcpasc  11127  remim  11541  mulreap  11545  readd  11550  remullem  11552  imadd  11558  cjadd  11565  bdtrilem  11920  fsummulc2  12130  binomlem  12165  tanval3ap  12396  sinadd  12418  tanaddap  12421  bezoutlemnewy  12688  dvdsmulgcd  12717  lcmgcdlem  12770  pythagtriplem1  12959  pcaddlem  13033  mul4sqlem  13087  tangtx  15695  rpmulcxp  15766  rpcxpmul2  15770  binom4  15836  lgseisenlem2  15936  2lgsoddprmlem2  15971  2sqlem4  15983  2sqlem8  15988