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

Theorem adddid 7754
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 7716 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
51, 2, 3, 4syl3anc 1199 1 (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1314  wcel 1463  (class class class)co 5740  cc 7582   + caddc 7587   · cmul 7589
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 7688
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  subdi  8111  mulreim  8329  apadd1  8333  conjmulap  8449  cju  8676  flhalf  10015  modqcyc  10072  addmodlteq  10111  binom2  10343  binom3  10349  sqoddm1div8  10384  bcpasc  10452  remim  10572  mulreap  10576  readd  10581  remullem  10583  imadd  10589  cjadd  10596  bdtrilem  10950  fsummulc2  11157  binomlem  11192  tanval3ap  11320  sinadd  11342  tanaddap  11345  bezoutlemnewy  11580  dvdsmulgcd  11609  lcmgcdlem  11654
  Copyright terms: Public domain W3C validator