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

Theorem adddi 7537
Description: Alias for ax-distr 7512, for naming consistency with adddii 7561. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
adddi ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))

Proof of Theorem adddi
StepHypRef Expression
1 ax-distr 7512 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 925   = wceq 1290  wcel 1439  (class class class)co 5668  cc 7411   + caddc 7416   · cmul 7418
This theorem was proved from axioms:  ax-distr 7512
This theorem is referenced by:  adddir  7542  adddii  7561  adddid  7575  muladd11  7678  cnegex  7723  muladd  7925  nnmulcl  8506  expmul  10063  bernneq  10137  sqoddm1div8  10169  iisermulc2  10791  efexp  11035  efi4p  11071  sinadd  11090  cosadd  11091  cos2tsin  11105  cos01bnd  11112  absefib  11123  efieq1re  11124  demoivreALT  11126  odd2np1  11214  opoe  11236  opeo  11238  gcdmultiple  11350
  Copyright terms: Public domain W3C validator