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

Theorem exlimdvv 1897
Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 31-Jul-1995.)
Hypothesis
Ref Expression
exlimdvv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
exlimdvv (𝜑 → (∃𝑥𝑦𝜓𝜒))
Distinct variable groups:   𝜒,𝑥   𝜑,𝑥   𝜒,𝑦   𝜑,𝑦
Allowed substitution hints:   𝜓(𝑥,𝑦)

Proof of Theorem exlimdvv
StepHypRef Expression
1 exlimdvv.1 . . 3 (𝜑 → (𝜓𝜒))
21exlimdv 1819 . 2 (𝜑 → (∃𝑦𝜓𝜒))
32exlimdv 1819 1 (𝜑 → (∃𝑥𝑦𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1447  ax-gen 1449  ax-ie2 1494  ax-17 1526
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  euotd  4250  funopg  5245  th3qlem1  6630  fundmen  6799  sbthlemi10  6958  addnq0mo  7424  mulnq0mo  7425  genprndl  7498  genprndu  7499  genpdisj  7500  mullocpr  7548  addsrmo  7720  mulsrmo  7721  cnm  7809  summodc  11362  fsum2dlemstep  11413  prodmodc  11557  fprod2dlemstep  11601  txbasval  13400
  Copyright terms: Public domain W3C validator