Theorem adddid 7944

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

Syntax hints:   → wi 4   = wceq 1348   ∈ wcel 2141  (class class class)co 5853  ℂcc 7772   + caddc 7777   · cmul 7779

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

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  subdi  8304  mulreim  8523  apadd1  8527  conjmulap  8646  cju  8877  flhalf  10258  modqcyc  10315  addmodlteq  10354  binom2  10587  binom3  10593  sqoddm1div8  10629  bcpasc  10700  remim  10824  mulreap  10828  readd  10833  remullem  10835  imadd  10841  cjadd  10848  bdtrilem  11202  fsummulc2  11411  binomlem  11446  tanval3ap  11677  sinadd  11699  tanaddap  11702  bezoutlemnewy  11951  dvdsmulgcd  11980  lcmgcdlem  12031  pythagtriplem1  12219  pcaddlem  12292  mul4sqlem  12345  tangtx  13553  rpmulcxp  13624  binom4  13691  2sqlem4  13748  2sqlem8  13753