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

Theorem exlimivv 1825
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 1535 . 2 (∃𝑦𝜑𝜓)
32exlimiv 1535 1 (∃𝑥𝑦𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1427
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-gen 1384  ax-ie2 1429  ax-17 1465
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  cgsex2g  2656  cgsex4g  2657  opabss  3908  copsexg  4080  elopab  4094  epelg  4126  0nelelxp  4480  elvvuni  4515  optocl  4527  xpsspw  4563  relopabi  4576  relop  4599  elreldm  4674  xpmlem  4865  dfco2a  4944  unielrel  4971  oprabid  5695  1stval2  5940  2ndval2  5941  xp1st  5950  xp2nd  5951  poxp  6011  rntpos  6036  dftpos4  6042  tpostpos  6043  tfrlem7  6096  th3qlem2  6409  ener  6550  domtr  6556  unen  6587  xpsnen  6591  mapen  6616  ltdcnq  7017  archnqq  7037  enq0tr  7054  nqnq0pi  7058  nqnq0  7061  nqpnq0nq  7073  nqnq0a  7074  nqnq0m  7075  nq0m0r  7076  nq0a0  7077  nq02m  7085  prarloc  7123  axaddcl  7462  axmulcl  7464  hashfacen  10302  bj-inex  12071
  Copyright terms: Public domain W3C validator