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

Theorem adddid 7502
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 7464 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
51, 2, 3, 4syl3anc 1174 1 (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1289  wcel 1438  (class class class)co 5644  cc 7338   + caddc 7343   · cmul 7345
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-distr 7439
This theorem depends on definitions:  df-bi 115  df-3an 926
This theorem is referenced by:  subdi  7853  mulreim  8071  apadd1  8075  conjmulap  8186  cju  8411  flhalf  9697  modqcyc  9754  addmodlteq  9793  binom2  10053  binom3  10059  sqoddm1div8  10094  bcpasc  10162  remim  10282  mulreap  10286  readd  10291  remullem  10293  imadd  10299  cjadd  10306  fsummulc2  10829  binomlem  10864  tanval3ap  10992  sinadd  11014  tanaddap  11017  bezoutlemnewy  11250  dvdsmulgcd  11279  lcmgcdlem  11324
  Copyright terms: Public domain W3C validator