Theorem exlimivv 1876

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

Step	Hyp	Ref	Expression
1		exlimivv.1	. . 3 |- ( ph -> ps )
2	1	exlimiv 1578	. 2 |- ( E. y ph -> ps )
3	2	exlimiv 1578	1 |- ( E. x E. y ph -> ps )

Syntax hints:   -> wi 4   E.wex 1472

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1429  ax-ie2 1474  ax-17 1506

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  cgsex2g  2748  cgsex4g  2749  opabss  4028  copsexg  4204  elopab  4218  epelg  4250  0nelelxp  4614  elvvuni  4649  optocl  4661  xpsspw  4697  relopabi  4711  relop  4735  elreldm  4811  xpmlem  5005  dfco2a  5085  unielrel  5112  oprabid  5850  1stval2  6100  2ndval2  6101  xp1st  6110  xp2nd  6111  poxp  6176  rntpos  6201  dftpos4  6207  tpostpos  6208  tfrlem7  6261  th3qlem2  6580  ener  6721  domtr  6727  unen  6758  xpsnen  6763  mapen  6788  ltdcnq  7311  archnqq  7331  enq0tr  7348  nqnq0pi  7352  nqnq0  7355  nqpnq0nq  7367  nqnq0a  7368  nqnq0m  7369  nq0m0r  7370  nq0a0  7371  nq02m  7379  prarloc  7417  axaddcl  7778  axmulcl  7780  hashfacen  10700  bj-inex  13453