Theorem exlimivv 1889

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

Syntax hints:   -> wi 4   E.wex 1485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1442  ax-ie2 1487  ax-17 1519

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  cgsex2g  2766  cgsex4g  2767  opabss  4053  copsexg  4229  elopab  4243  epelg  4275  0nelelxp  4640  elvvuni  4675  optocl  4687  xpsspw  4723  relopabi  4737  relop  4761  elreldm  4837  xpmlem  5031  dfco2a  5111  unielrel  5138  oprabid  5885  1stval2  6134  2ndval2  6135  xp1st  6144  xp2nd  6145  poxp  6211  rntpos  6236  dftpos4  6242  tpostpos  6243  tfrlem7  6296  th3qlem2  6616  ener  6757  domtr  6763  unen  6794  xpsnen  6799  mapen  6824  ltdcnq  7359  archnqq  7379  enq0tr  7396  nqnq0pi  7400  nqnq0  7403  nqpnq0nq  7415  nqnq0a  7416  nqnq0m  7417  nq0m0r  7418  nq0a0  7419  nq02m  7427  prarloc  7465  axaddcl  7826  axmulcl  7828  hashfacen  10771  bj-inex  13942