Theorem adddid 7982

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2148  (class class class)co 5875  ℂcc 7809   + caddc 7814   · cmul 7816

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 7915

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

This theorem is referenced by:  subdi  8342  mulreim  8561  apadd1  8565  conjmulap  8686  cju  8918  flhalf  10302  modqcyc  10359  addmodlteq  10398  binom2  10632  binom3  10638  sqoddm1div8  10674  bcpasc  10746  remim  10869  mulreap  10873  readd  10878  remullem  10880  imadd  10886  cjadd  10893  bdtrilem  11247  fsummulc2  11456  binomlem  11491  tanval3ap  11722  sinadd  11744  tanaddap  11747  bezoutlemnewy  11997  dvdsmulgcd  12026  lcmgcdlem  12077  pythagtriplem1  12265  pcaddlem  12338  mul4sqlem  12391  tangtx  14262  rpmulcxp  14333  binom4  14400  lgseisenlem2  14454  2lgsoddprmlem2  14457  2sqlem4  14468  2sqlem8  14473