Theorem adddid 8159

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 5994  ℂcc 7985   + caddc 7990   · cmul 7992

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 8091

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

This theorem is referenced by:  subdi  8519  mulreim  8739  apadd1  8743  conjmulap  8864  cju  9096  flhalf  10509  modqcyc  10568  addmodlteq  10607  binom2  10860  binom3  10866  sqoddm1div8  10902  bcpasc  10975  remim  11357  mulreap  11361  readd  11366  remullem  11368  imadd  11374  cjadd  11381  bdtrilem  11736  fsummulc2  11945  binomlem  11980  tanval3ap  12211  sinadd  12233  tanaddap  12236  bezoutlemnewy  12503  dvdsmulgcd  12532  lcmgcdlem  12585  pythagtriplem1  12774  pcaddlem  12848  mul4sqlem  12902  tangtx  15497  rpmulcxp  15568  rpcxpmul2  15572  binom4  15638  lgseisenlem2  15735  2lgsoddprmlem2  15770  2sqlem4  15782  2sqlem8  15787