Theorem adddid 7502

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

Syntax hints:   → wi 4   = wceq 1289   ∈ wcel 1438  (class class class)co 5644  ℂcc 7338   + caddc 7343   · cmul 7345

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-distr 7439

This theorem depends on definitions:  df-bi 115  df-3an 926

This theorem is referenced by:  subdi  7853  mulreim  8071  apadd1  8075  conjmulap  8186  cju  8411  flhalf  9697  modqcyc  9754  addmodlteq  9793  binom2  10053  binom3  10059  sqoddm1div8  10094  bcpasc  10162  remim  10282  mulreap  10286  readd  10291  remullem  10293  imadd  10299  cjadd  10306  fsummulc2  10829  binomlem  10864  tanval3ap  10992  sinadd  11014  tanaddap  11017  bezoutlemnewy  11250  dvdsmulgcd  11279  lcmgcdlem  11324