ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  exlimivv Unicode 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  |-  ( 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 1505 . 2  |-  ( E. y ph  ->  ps )
32exlimiv 1505 1  |-  ( E. x E. y ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.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  3849  copsexg  4009  elopab  4023  epelg  4055  0nelelxp  4401  elvvuni  4432  optocl  4444  xpsspw  4478  relopabi  4491  relop  4514  elreldm  4588  xpmlem  4772  dfco2a  4849  unielrel  4873  oprabid  5565  1stval2  5810  2ndval2  5811  xp1st  5820  xp2nd  5821  poxp  5881  rntpos  5903  dftpos4  5909  tpostpos  5910  tfrlem7  5964  th3qlem2  6240  ener  6290  domtr  6296  unen  6324  xpsnen  6326  ltdcnq  6553  archnqq  6573  enq0tr  6590  nqnq0pi  6594  nqnq0  6597  nqpnq0nq  6609  nqnq0a  6610  nqnq0m  6611  nq0m0r  6612  nq0a0  6613  nq02m  6621  prarloc  6659  axaddcl  6998  axmulcl  7000  bj-inex  10414
  Copyright terms: Public domain W3C validator