ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  adddid GIF version

Theorem adddid 7903
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
StepHypRef Expression
1 addcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcld.2 . 2 (𝜑𝐵 ∈ ℂ)
3 addassd.3 . 2 (𝜑𝐶 ∈ ℂ)
4 adddi 7865 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
51, 2, 3, 4syl3anc 1220 1 (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1335  wcel 2128  (class class class)co 5825  cc 7731   + caddc 7736   · cmul 7738
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-distr 7837
This theorem depends on definitions:  df-bi 116  df-3an 965
This theorem is referenced by:  subdi  8261  mulreim  8480  apadd1  8484  conjmulap  8603  cju  8833  flhalf  10205  modqcyc  10262  addmodlteq  10301  binom2  10533  binom3  10539  sqoddm1div8  10575  bcpasc  10644  remim  10764  mulreap  10768  readd  10773  remullem  10775  imadd  10781  cjadd  10788  bdtrilem  11142  fsummulc2  11349  binomlem  11384  tanval3ap  11615  sinadd  11637  tanaddap  11640  bezoutlemnewy  11884  dvdsmulgcd  11913  lcmgcdlem  11958  pythagtriplem1  12144  tangtx  13201  rpmulcxp  13272  binom4  13338
  Copyright terms: Public domain W3C validator