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

Theorem adddid 8046
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 8006 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
51, 2, 3, 4syl3anc 1249 1 (𝜑 → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1364  wcel 2164  (class class class)co 5919  cc 7872   + caddc 7877   · cmul 7879
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 7978
This theorem depends on definitions:  df-bi 117  df-3an 982
This theorem is referenced by:  subdi  8406  mulreim  8625  apadd1  8629  conjmulap  8750  cju  8982  flhalf  10374  modqcyc  10433  addmodlteq  10472  binom2  10725  binom3  10731  sqoddm1div8  10767  bcpasc  10840  remim  11007  mulreap  11011  readd  11016  remullem  11018  imadd  11024  cjadd  11031  bdtrilem  11385  fsummulc2  11594  binomlem  11629  tanval3ap  11860  sinadd  11882  tanaddap  11885  bezoutlemnewy  12136  dvdsmulgcd  12165  lcmgcdlem  12218  pythagtriplem1  12406  pcaddlem  12480  mul4sqlem  12534  tangtx  15014  rpmulcxp  15085  binom4  15152  lgseisenlem2  15228  2lgsoddprmlem2  15263  2sqlem4  15275  2sqlem8  15280
  Copyright terms: Public domain W3C validator