Theorem exlimivv 1908

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

Syntax hints:   -> wi 4   E.wex 1503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1460  ax-ie2 1505  ax-17 1537

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cgsex2g  2796  cgsex4g  2797  opabss  4094  copsexg  4274  elopab  4289  epelg  4322  0nelelxp  4689  elvvuni  4724  optocl  4736  xpsspw  4772  relopabi  4788  relop  4813  elreldm  4889  xpmlem  5087  dfco2a  5167  unielrel  5194  oprabid  5951  1stval2  6210  2ndval2  6211  xp1st  6220  xp2nd  6221  poxp  6287  rntpos  6312  dftpos4  6318  tpostpos  6319  tfrlem7  6372  th3qlem2  6694  ener  6835  domtr  6841  unen  6872  xpsnen  6877  mapen  6904  ltdcnq  7459  archnqq  7479  enq0tr  7496  nqnq0pi  7500  nqnq0  7503  nqpnq0nq  7515  nqnq0a  7516  nqnq0m  7517  nq0m0r  7518  nq0a0  7519  nq02m  7527  prarloc  7565  axaddcl  7926  axmulcl  7928  hashfacen  10910  bj-inex  15469