Theorem exlimivv 1884

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 1586	. 2 |- ( E. y ph -> ps )
3	2	exlimiv 1586	1 |- ( E. x E. y ph -> ps )

Syntax hints:   -> wi 4   E.wex 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1437  ax-ie2 1482  ax-17 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  cgsex2g  2762  cgsex4g  2763  opabss  4046  copsexg  4222  elopab  4236  epelg  4268  0nelelxp  4633  elvvuni  4668  optocl  4680  xpsspw  4716  relopabi  4730  relop  4754  elreldm  4830  xpmlem  5024  dfco2a  5104  unielrel  5131  oprabid  5874  1stval2  6123  2ndval2  6124  xp1st  6133  xp2nd  6134  poxp  6200  rntpos  6225  dftpos4  6231  tpostpos  6232  tfrlem7  6285  th3qlem2  6604  ener  6745  domtr  6751  unen  6782  xpsnen  6787  mapen  6812  ltdcnq  7338  archnqq  7358  enq0tr  7375  nqnq0pi  7379  nqnq0  7382  nqpnq0nq  7394  nqnq0a  7395  nqnq0m  7396  nq0m0r  7397  nq0a0  7398  nq02m  7406  prarloc  7444  axaddcl  7805  axmulcl  7807  hashfacen  10749  bj-inex  13799