Theorem adddid 8351

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 8312	. 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 8178   + caddc 8183   · cmul 8185

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 8284

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

This theorem is used by:  subdi  8714  mulreim  8935  apadd1  8939  conjmulap  9062  cju  9294  flhalf  10751  modqcyc  10810  addmodlteq  10849  binom2  11102  binom3  11108  sqoddm1div8  11145  bcpasc  11219  hashf1lem2  11301  remim  11640  mulreap  11644  readd  11649  remullem  11651  imadd  11657  cjadd  11664  bdtrilem  12023  fsummulc2  12233  binomlem  12268  tanval3ap  12499  sinadd  12521  tanaddap  12524  bezoutlemnewy  12791  dvdsmulgcd  12820  lcmgcdlem  12873  pythagtriplem1  13066  pcaddlem  13140  mul4sqlem  13194  tangtx  15992  rpmulcxp  16067  rpcxpmul2  16071  binom4  16141  chtqub  16218  lgseisenlem2  16312  2lgsoddprmlem2  16347  2sqlem4  16359  2sqlem8  16364