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

Theorem rexlimivv 2495
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 17-Feb-2004.)
Hypothesis
Ref Expression
rexlimivv.1 ((𝑥𝐴𝑦𝐵) → (𝜑𝜓))
Assertion
Ref Expression
rexlimivv (∃𝑥𝐴𝑦𝐵 𝜑𝜓)
Distinct variable groups:   𝑥,𝑦,𝜓   𝑦,𝐴
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥)   𝐵(𝑥,𝑦)

Proof of Theorem rexlimivv
StepHypRef Expression
1 rexlimivv.1 . . 3 ((𝑥𝐴𝑦𝐵) → (𝜑𝜓))
21rexlimdva 2490 . 2 (𝑥𝐴 → (∃𝑦𝐵 𝜑𝜓))
32rexlimiv 2484 1 (∃𝑥𝐴𝑦𝐵 𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 1439  wrex 2361
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 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-17 1465  ax-ial 1473  ax-i5r 1474
This theorem depends on definitions:  df-bi 116  df-nf 1396  df-ral 2365  df-rex 2366
This theorem is referenced by:  opelxp  4481  f1o2ndf1  6007  xpdom2  6601  distrlem5prl  7206  distrlem5pru  7207  mulid1  7546  cnegex  7721  recexap  8183  creur  8480  creui  8481  cju  8482  elz2  8879  qre  9171  qaddcl  9181  qnegcl  9182  qmulcl  9183  qreccl  9188  replim  10354  odd2np1  11212  opoe  11234  omoe  11235  opeo  11236  omeo  11237  qredeu  11418
  Copyright terms: Public domain W3C validator