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

Theorem rexlimdvv 2614
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 2606 . 2 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓𝜒))
43rexlimdva 2607 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wcel 2160  wrex 2469
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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-i5r 1546
This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473  df-rex 2474
This theorem is referenced by:  rexlimdvva  2615  f1oiso2  5844  xpdom2  6849  genpcdl  7537  genpcuu  7538  distrlem1prl  7600  distrlem1pru  7601  distrlem5prl  7604  distrlem5pru  7605  recexprlemss1l  7653  recexprlemss1u  7654  qaddcl  9654  qmulcl  9656  summodc  11410  dvdsgcd  12032  gcddiv  12039  pceu  12314  pcqcl  12325  txcnp  14174  blssps  14330  blss  14331  tgqioo  14450
  Copyright terms: Public domain W3C validator