Theorem adddid 7919

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

Syntax hints:   → wi 4   = wceq 1343   ∈ wcel 2136  (class class class)co 5841  ℂcc 7747   + caddc 7752   · cmul 7754

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 7853

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

This theorem is referenced by:  subdi  8279  mulreim  8498  apadd1  8502  conjmulap  8621  cju  8852  flhalf  10233  modqcyc  10290  addmodlteq  10329  binom2  10562  binom3  10568  sqoddm1div8  10604  bcpasc  10675  remim  10798  mulreap  10802  readd  10807  remullem  10809  imadd  10815  cjadd  10822  bdtrilem  11176  fsummulc2  11385  binomlem  11420  tanval3ap  11651  sinadd  11673  tanaddap  11676  bezoutlemnewy  11925  dvdsmulgcd  11954  lcmgcdlem  12005  pythagtriplem1  12193  pcaddlem  12266  mul4sqlem  12319  tangtx  13359  rpmulcxp  13430  binom4  13497  2sqlem4  13554  2sqlem8  13559