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

Theorem rexlimivv 2600
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 2594 . 2 (𝑥𝐴 → (∃𝑦𝐵 𝜑𝜓))
32rexlimiv 2588 1 (∃𝑥𝐴𝑦𝐵 𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wcel 2148  wrex 2456
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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460  df-rex 2461
This theorem is referenced by:  opelxp  4658  f1o2ndf1  6231  xpdom2  6833  distrlem5prl  7587  distrlem5pru  7588  mulrid  7956  cnegex  8137  recexap  8612  creur  8918  creui  8919  cju  8920  elz2  9326  qre  9627  qaddcl  9637  qnegcl  9638  qmulcl  9639  qreccl  9644  elpqb  9651  replim  10870  prodmodc  11588  odd2np1  11880  opoe  11902  omoe  11903  opeo  11904  omeo  11905  qredeu  12099  pythagtriplem1  12267  pcz  12333  4sqlem1  12388  4sqlem2  12389  4sqlem4  12392  mul4sq  12394  txuni2  13841  blssioo  14130  tgioo  14131  2sqlem2  14547  mul2sq  14548  2sqlem7  14553
  Copyright terms: Public domain W3C validator