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

Theorem exlimivv 1919
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 1620 . 2 (∃𝑦𝜑𝜓)
32exlimiv 1620 1 (∃𝑥𝑦𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1514
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1471  ax-ie2 1516  ax-17 1548
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  cgsex2g  2807  cgsex4g  2808  opabss  4107  copsexg  4287  elopab  4303  epelg  4336  0nelelxp  4703  elvvuni  4738  optocl  4750  xpsspw  4786  relopabi  4802  relop  4827  elreldm  4903  xpmlem  5102  dfco2a  5182  unielrel  5209  oprabid  5975  1stval2  6240  2ndval2  6241  xp1st  6250  xp2nd  6251  poxp  6317  rntpos  6342  dftpos4  6348  tpostpos  6349  tfrlem7  6402  th3qlem2  6724  ener  6870  domtr  6876  unen  6907  xpsnen  6915  mapen  6942  ltdcnq  7509  archnqq  7529  enq0tr  7546  nqnq0pi  7550  nqnq0  7553  nqpnq0nq  7565  nqnq0a  7566  nqnq0m  7567  nq0m0r  7568  nq0a0  7569  nq02m  7577  prarloc  7615  axaddcl  7976  axmulcl  7978  hashfacen  10979  fundm2domnop0  10988  fsumdvdsmul  15405  bj-inex  15776
  Copyright terms: Public domain W3C validator