Theorem exlimivv 1868

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

Syntax hints:   -> wi 4   E.wex 1468

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  cgsex2g  2717  cgsex4g  2718  opabss  3987  copsexg  4161  elopab  4175  epelg  4207  0nelelxp  4563  elvvuni  4598  optocl  4610  xpsspw  4646  relopabi  4660  relop  4684  elreldm  4760  xpmlem  4954  dfco2a  5034  unielrel  5061  oprabid  5796  1stval2  6046  2ndval2  6047  xp1st  6056  xp2nd  6057  poxp  6122  rntpos  6147  dftpos4  6153  tpostpos  6154  tfrlem7  6207  th3qlem2  6525  ener  6666  domtr  6672  unen  6703  xpsnen  6708  mapen  6733  ltdcnq  7198  archnqq  7218  enq0tr  7235  nqnq0pi  7239  nqnq0  7242  nqpnq0nq  7254  nqnq0a  7255  nqnq0m  7256  nq0m0r  7257  nq0a0  7258  nq02m  7266  prarloc  7304  axaddcl  7665  axmulcl  7667  hashfacen  10572  bj-inex  13094