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

Theorem exlimivv 1792
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 1505 . 2 (∃𝑦𝜑𝜓)
32exlimiv 1505 1 (∃𝑥𝑦𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1397
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-gen 1354  ax-ie2 1399  ax-17 1435
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  cgsex2g  2607  cgsex4g  2608  opabss  3848  copsexg  4008  elopab  4022  epelg  4054  0nelelxp  4400  elvvuni  4431  optocl  4443  xpsspw  4477  relopabi  4490  relop  4513  elreldm  4587  xpmlem  4771  dfco2a  4848  unielrel  4872  oprabid  5564  1stval2  5809  2ndval2  5810  xp1st  5819  xp2nd  5820  poxp  5880  rntpos  5902  dftpos4  5908  tpostpos  5909  tfrlem7  5963  th3qlem2  6239  ener  6289  domtr  6295  unen  6323  xpsnen  6325  ltdcnq  6552  archnqq  6572  enq0tr  6589  nqnq0pi  6593  nqnq0  6596  nqpnq0nq  6608  nqnq0a  6609  nqnq0m  6610  nq0m0r  6611  nq0a0  6612  nq02m  6620  prarloc  6658  axaddcl  6997  axmulcl  6999  bj-inex  10386
  Copyright terms: Public domain W3C validator