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

Theorem exlimivv 1908
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 1609 . 2 (∃𝑦𝜑𝜓)
32exlimiv 1609 1 (∃𝑥𝑦𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1503
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1460  ax-ie2 1505  ax-17 1537
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  cgsex2g  2788  cgsex4g  2789  opabss  4082  copsexg  4262  elopab  4276  epelg  4308  0nelelxp  4673  elvvuni  4708  optocl  4720  xpsspw  4756  relopabi  4770  relop  4795  elreldm  4871  xpmlem  5067  dfco2a  5147  unielrel  5174  oprabid  5929  1stval2  6181  2ndval2  6182  xp1st  6191  xp2nd  6192  poxp  6258  rntpos  6283  dftpos4  6289  tpostpos  6290  tfrlem7  6343  th3qlem2  6665  ener  6806  domtr  6812  unen  6843  xpsnen  6848  mapen  6875  ltdcnq  7427  archnqq  7447  enq0tr  7464  nqnq0pi  7468  nqnq0  7471  nqpnq0nq  7483  nqnq0a  7484  nqnq0m  7485  nq0m0r  7486  nq0a0  7487  nq02m  7495  prarloc  7533  axaddcl  7894  axmulcl  7896  hashfacen  10851  bj-inex  15137
  Copyright terms: Public domain W3C validator