Theorem adddid 8204

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

Syntax hints:   → wi 4   = wceq 1397   ∈ wcel 2202  (class class class)co 6018  ℂcc 8030   + caddc 8035   · cmul 8037

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 8136

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

This theorem is referenced by:  subdi  8564  mulreim  8784  apadd1  8788  conjmulap  8909  cju  9141  flhalf  10563  modqcyc  10622  addmodlteq  10661  binom2  10914  binom3  10920  sqoddm1div8  10956  bcpasc  11029  remim  11425  mulreap  11429  readd  11434  remullem  11436  imadd  11442  cjadd  11449  bdtrilem  11804  fsummulc2  12014  binomlem  12049  tanval3ap  12280  sinadd  12302  tanaddap  12305  bezoutlemnewy  12572  dvdsmulgcd  12601  lcmgcdlem  12654  pythagtriplem1  12843  pcaddlem  12917  mul4sqlem  12971  tangtx  15568  rpmulcxp  15639  rpcxpmul2  15643  binom4  15709  lgseisenlem2  15806  2lgsoddprmlem2  15841  2sqlem4  15853  2sqlem8  15858