Theorem adddid 8112

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

Syntax hints:   → wi 4   = wceq 1373   ∈ wcel 2177  (class class class)co 5956  ℂcc 7938   + caddc 7943   · cmul 7945

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 8044

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

This theorem is referenced by:  subdi  8472  mulreim  8692  apadd1  8696  conjmulap  8817  cju  9049  flhalf  10462  modqcyc  10521  addmodlteq  10560  binom2  10813  binom3  10819  sqoddm1div8  10855  bcpasc  10928  remim  11241  mulreap  11245  readd  11250  remullem  11252  imadd  11258  cjadd  11265  bdtrilem  11620  fsummulc2  11829  binomlem  11864  tanval3ap  12095  sinadd  12117  tanaddap  12120  bezoutlemnewy  12387  dvdsmulgcd  12416  lcmgcdlem  12469  pythagtriplem1  12658  pcaddlem  12732  mul4sqlem  12786  tangtx  15380  rpmulcxp  15451  rpcxpmul2  15455  binom4  15521  lgseisenlem2  15618  2lgsoddprmlem2  15653  2sqlem4  15665  2sqlem8  15670