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

Theorem exlimivv 1824
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 1-Aug-1995.)
Hypothesis
Ref Expression
exlimivv.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
exlimivv  |-  ( E. x E. y ph  ->  ps )
Distinct variable groups:    ps, x    ps, y
Allowed substitution hints:    ph( x, y)

Proof of Theorem exlimivv
StepHypRef Expression
1 exlimivv.1 . . 3  |-  ( ph  ->  ps )
21exlimiv 1534 . 2  |-  ( E. y ph  ->  ps )
32exlimiv 1534 1  |-  ( E. x E. y ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1426
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-gen 1383  ax-ie2 1428  ax-17 1464
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  cgsex2g  2655  cgsex4g  2656  opabss  3894  copsexg  4062  elopab  4076  epelg  4108  0nelelxp  4456  elvvuni  4490  optocl  4502  xpsspw  4538  relopabi  4551  relop  4574  elreldm  4649  xpmlem  4839  dfco2a  4918  unielrel  4945  oprabid  5663  1stval2  5908  2ndval2  5909  xp1st  5918  xp2nd  5919  poxp  5979  rntpos  6004  dftpos4  6010  tpostpos  6011  tfrlem7  6064  th3qlem2  6375  ener  6476  domtr  6482  unen  6513  xpsnen  6517  mapen  6542  ltdcnq  6935  archnqq  6955  enq0tr  6972  nqnq0pi  6976  nqnq0  6979  nqpnq0nq  6991  nqnq0a  6992  nqnq0m  6993  nq0m0r  6994  nq0a0  6995  nq02m  7003  prarloc  7041  axaddcl  7380  axmulcl  7382  hashfacen  10206  bj-inex  11444
  Copyright terms: Public domain W3C validator