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

Theorem rexlimdvv 2611
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 22-Jul-2004.)
Hypothesis
Ref Expression
rexlimdvv.1 (𝜑 → ((𝑥𝐴𝑦𝐵) → (𝜓𝜒)))
Assertion
Ref Expression
rexlimdvv (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓𝜒))
Distinct variable groups:   𝑥,𝑦,𝜑   𝜒,𝑥,𝑦   𝑦,𝐴
Allowed substitution hints:   𝜓(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem rexlimdvv
StepHypRef Expression
1 rexlimdvv.1 . . . 4 (𝜑 → ((𝑥𝐴𝑦𝐵) → (𝜓𝜒)))
21expdimp 259 . . 3 ((𝜑𝑥𝐴) → (𝑦𝐵 → (𝜓𝜒)))
32rexlimdv 2603 . 2 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓𝜒))
43rexlimdva 2604 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wcel 2158  wrex 2466
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-5 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-i5r 1545
This theorem depends on definitions:  df-bi 117  df-nf 1471  df-ral 2470  df-rex 2471
This theorem is referenced by:  rexlimdvva  2612  f1oiso2  5841  xpdom2  6844  genpcdl  7531  genpcuu  7532  distrlem1prl  7594  distrlem1pru  7595  distrlem5prl  7598  distrlem5pru  7599  recexprlemss1l  7647  recexprlemss1u  7648  qaddcl  9648  qmulcl  9650  summodc  11404  dvdsgcd  12026  gcddiv  12033  pceu  12308  pcqcl  12319  txcnp  14011  blssps  14167  blss  14168  tgqioo  14287
  Copyright terms: Public domain W3C validator