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

Theorem exlimivv 1776
 Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 1-Aug-1995.)
Hypothesis
Ref Expression
exlimivv.1 (𝜑𝜓)
Assertion
Ref Expression
exlimivv (∃𝑥𝑦𝜑𝜓)
Distinct variable groups:   𝜓,𝑥   𝜓,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)

Proof of Theorem exlimivv
StepHypRef Expression
1 exlimivv.1 . . 3 (𝜑𝜓)
21exlimiv 1489 . 2 (∃𝑦𝜑𝜓)
32exlimiv 1489 1 (∃𝑥𝑦𝜑𝜓)
 Colors of variables: wff set class Syntax hints:   → wi 4  ∃wex 1381 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-gen 1338  ax-ie2 1383  ax-17 1419 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  cgsex2g  2590  cgsex4g  2591  opabss  3821  copsexg  3981  elopab  3995  epelg  4027  0nelelxp  4373  elvvuni  4404  optocl  4416  xpsspw  4450  relopabi  4463  relop  4486  elreldm  4560  xpmlem  4744  dfco2a  4821  unielrel  4845  oprabid  5537  1stval2  5782  2ndval2  5783  xp1st  5792  xp2nd  5793  poxp  5853  rntpos  5872  dftpos4  5878  tpostpos  5879  tfrlem7  5933  th3qlem2  6209  ener  6259  domtr  6265  unen  6293  xpsnen  6295  ltdcnq  6495  archnqq  6515  enq0tr  6532  nqnq0pi  6536  nqnq0  6539  nqpnq0nq  6551  nqnq0a  6552  nqnq0m  6553  nq0m0r  6554  nq0a0  6555  nq02m  6563  prarloc  6601  axaddcl  6940  axmulcl  6942  bj-inex  10027
 Copyright terms: Public domain W3C validator