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

Theorem rexlimivv 2455
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 2450 . 2 (𝑥𝐴 → (∃𝑦𝐵 𝜑𝜓))
32rexlimiv 2444 1 (∃𝑥𝐴𝑦𝐵 𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wcel 1409  wrex 2324
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-i5r 1444
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-ral 2328  df-rex 2329
This theorem is referenced by:  opelxp  4402  f1o2ndf1  5877  xpdom2  6336  distrlem5prl  6742  distrlem5pru  6743  mulid1  7082  cnegex  7252  recexap  7708  creur  7987  creui  7988  cju  7989  elz2  8370  qre  8657  qaddcl  8667  qnegcl  8668  qmulcl  8669  qreccl  8674  replim  9687  odd2np1  10184  opoe  10207  omoe  10208  opeo  10209  omeo  10210
  Copyright terms: Public domain W3C validator