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

Theorem rexlimdvv 2509
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 256 . . 3 ((𝜑𝑥𝐴) → (𝑦𝐵 → (𝜓𝜒)))
32rexlimdv 2501 . 2 ((𝜑𝑥𝐴) → (∃𝑦𝐵 𝜓𝜒))
43rexlimdva 2502 1 (𝜑 → (∃𝑥𝐴𝑦𝐵 𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 1445  wrex 2371
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-4 1452  ax-17 1471  ax-ial 1479  ax-i5r 1480
This theorem depends on definitions:  df-bi 116  df-nf 1402  df-ral 2375  df-rex 2376
This theorem is referenced by:  rexlimdvva  2510  f1oiso2  5644  xpdom2  6627  genpcdl  7175  genpcuu  7176  distrlem1prl  7238  distrlem1pru  7239  distrlem5prl  7242  distrlem5pru  7243  recexprlemss1l  7291  recexprlemss1u  7292  qaddcl  9219  qmulcl  9221  summodc  10941  dvdsgcd  11443  gcddiv  11450  blssps  12228  blss  12229  tgqioo  12336
  Copyright terms: Public domain W3C validator