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  4302  epelg  4335  0nelelxp  4702  elvvuni  4737  optocl  4749  xpsspw  4785  relopabi  4801  relop  4826  elreldm  4902  xpmlem  5100  dfco2a  5180  unielrel  5207  oprabid  5966  1stval2  6231  2ndval2  6232  xp1st  6241  xp2nd  6242  poxp  6308  rntpos  6333  dftpos4  6339  tpostpos  6340  tfrlem7  6393  th3qlem2  6715  ener  6856  domtr  6862  unen  6893  xpsnen  6898  mapen  6925  ltdcnq  7492  archnqq  7512  enq0tr  7529  nqnq0pi  7533  nqnq0  7536  nqpnq0nq  7548  nqnq0a  7549  nqnq0m  7550  nq0m0r  7551  nq0a0  7552  nq02m  7560  prarloc  7598  axaddcl  7959  axmulcl  7961  hashfacen  10962  fsumdvdsmul  15381  bj-inex  15707
  Copyright terms: Public domain W3C validator