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

Theorem exlimivv 1896
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 1598 . 2  |-  ( E. y ph  ->  ps )
32exlimiv 1598 1  |-  ( E. x E. y ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1449  ax-ie2 1494  ax-17 1526
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  cgsex2g  2773  cgsex4g  2774  opabss  4067  copsexg  4244  elopab  4258  epelg  4290  0nelelxp  4655  elvvuni  4690  optocl  4702  xpsspw  4738  relopabi  4752  relop  4777  elreldm  4853  xpmlem  5049  dfco2a  5129  unielrel  5156  oprabid  5906  1stval2  6155  2ndval2  6156  xp1st  6165  xp2nd  6166  poxp  6232  rntpos  6257  dftpos4  6263  tpostpos  6264  tfrlem7  6317  th3qlem2  6637  ener  6778  domtr  6784  unen  6815  xpsnen  6820  mapen  6845  ltdcnq  7395  archnqq  7415  enq0tr  7432  nqnq0pi  7436  nqnq0  7439  nqpnq0nq  7451  nqnq0a  7452  nqnq0m  7453  nq0m0r  7454  nq0a0  7455  nq02m  7463  prarloc  7501  axaddcl  7862  axmulcl  7864  hashfacen  10811  bj-inex  14541
  Copyright terms: Public domain W3C validator