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

Theorem exlimivv 1848
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 1558 . 2  |-  ( E. y ph  ->  ps )
32exlimiv 1558 1  |-  ( E. x E. y ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1449
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-gen 1406  ax-ie2 1451  ax-17 1487
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  cgsex2g  2691  cgsex4g  2692  opabss  3950  copsexg  4124  elopab  4138  epelg  4170  0nelelxp  4526  elvvuni  4561  optocl  4573  xpsspw  4609  relopabi  4623  relop  4647  elreldm  4723  xpmlem  4915  dfco2a  4995  unielrel  5022  oprabid  5755  1stval2  6005  2ndval2  6006  xp1st  6015  xp2nd  6016  poxp  6081  rntpos  6106  dftpos4  6112  tpostpos  6113  tfrlem7  6166  th3qlem2  6484  ener  6625  domtr  6631  unen  6662  xpsnen  6666  mapen  6691  ltdcnq  7147  archnqq  7167  enq0tr  7184  nqnq0pi  7188  nqnq0  7191  nqpnq0nq  7203  nqnq0a  7204  nqnq0m  7205  nq0m0r  7206  nq0a0  7207  nq02m  7215  prarloc  7253  axaddcl  7593  axmulcl  7595  hashfacen  10466  bj-inex  12788
  Copyright terms: Public domain W3C validator