Theorem adddid 8044

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2164  (class class class)co 5918  ℂcc 7870   + caddc 7875   · cmul 7877

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 7976

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

This theorem is referenced by:  subdi  8404  mulreim  8623  apadd1  8627  conjmulap  8748  cju  8980  flhalf  10371  modqcyc  10430  addmodlteq  10469  binom2  10722  binom3  10728  sqoddm1div8  10764  bcpasc  10837  remim  11004  mulreap  11008  readd  11013  remullem  11015  imadd  11021  cjadd  11028  bdtrilem  11382  fsummulc2  11591  binomlem  11626  tanval3ap  11857  sinadd  11879  tanaddap  11882  bezoutlemnewy  12133  dvdsmulgcd  12162  lcmgcdlem  12215  pythagtriplem1  12403  pcaddlem  12477  mul4sqlem  12531  tangtx  14973  rpmulcxp  15044  binom4  15111  lgseisenlem2  15187  2lgsoddprmlem2  15194  2sqlem4  15205  2sqlem8  15210