Theorem adddid 8179

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

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200  (class class class)co 6007  ℂcc 8005   + caddc 8010   · cmul 8012

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 8111

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

This theorem is referenced by:  subdi  8539  mulreim  8759  apadd1  8763  conjmulap  8884  cju  9116  flhalf  10530  modqcyc  10589  addmodlteq  10628  binom2  10881  binom3  10887  sqoddm1div8  10923  bcpasc  10996  remim  11379  mulreap  11383  readd  11388  remullem  11390  imadd  11396  cjadd  11403  bdtrilem  11758  fsummulc2  11967  binomlem  12002  tanval3ap  12233  sinadd  12255  tanaddap  12258  bezoutlemnewy  12525  dvdsmulgcd  12554  lcmgcdlem  12607  pythagtriplem1  12796  pcaddlem  12870  mul4sqlem  12924  tangtx  15520  rpmulcxp  15591  rpcxpmul2  15595  binom4  15661  lgseisenlem2  15758  2lgsoddprmlem2  15793  2sqlem4  15805  2sqlem8  15810