Theorem adddid 8070

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

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167  (class class class)co 5925  ℂcc 7896   + caddc 7901   · cmul 7903

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 8002

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

This theorem is referenced by:  subdi  8430  mulreim  8650  apadd1  8654  conjmulap  8775  cju  9007  flhalf  10411  modqcyc  10470  addmodlteq  10509  binom2  10762  binom3  10768  sqoddm1div8  10804  bcpasc  10877  remim  11044  mulreap  11048  readd  11053  remullem  11055  imadd  11061  cjadd  11068  bdtrilem  11423  fsummulc2  11632  binomlem  11667  tanval3ap  11898  sinadd  11920  tanaddap  11923  bezoutlemnewy  12190  dvdsmulgcd  12219  lcmgcdlem  12272  pythagtriplem1  12461  pcaddlem  12535  mul4sqlem  12589  tangtx  15182  rpmulcxp  15253  rpcxpmul2  15257  binom4  15323  lgseisenlem2  15420  2lgsoddprmlem2  15455  2sqlem4  15467  2sqlem8  15472