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

Theorem exlimivv 1889
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 1591 . 2 (∃𝑦𝜑𝜓)
32exlimiv 1591 1 (∃𝑥𝑦𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1485
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1442  ax-ie2 1487  ax-17 1519
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  cgsex2g  2766  cgsex4g  2767  opabss  4051  copsexg  4227  elopab  4241  epelg  4273  0nelelxp  4638  elvvuni  4673  optocl  4685  xpsspw  4721  relopabi  4735  relop  4759  elreldm  4835  xpmlem  5029  dfco2a  5109  unielrel  5136  oprabid  5883  1stval2  6132  2ndval2  6133  xp1st  6142  xp2nd  6143  poxp  6209  rntpos  6234  dftpos4  6240  tpostpos  6241  tfrlem7  6294  th3qlem2  6613  ener  6754  domtr  6760  unen  6791  xpsnen  6796  mapen  6821  ltdcnq  7348  archnqq  7368  enq0tr  7385  nqnq0pi  7389  nqnq0  7392  nqpnq0nq  7404  nqnq0a  7405  nqnq0m  7406  nq0m0r  7407  nq0a0  7408  nq02m  7416  prarloc  7454  axaddcl  7815  axmulcl  7817  hashfacen  10760  bj-inex  13904
  Copyright terms: Public domain W3C validator