Theorem exlimivv 1920

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

Syntax hints:   -> wi 4   E.wex 1515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1472  ax-ie2 1517  ax-17 1549

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cgsex2g  2808  cgsex4g  2809  opabss  4109  copsexg  4289  elopab  4305  epelg  4338  0nelelxp  4705  elvvuni  4740  optocl  4752  xpsspw  4788  relopabi  4804  relop  4829  elreldm  4905  xpmlem  5104  dfco2a  5184  unielrel  5211  oprabid  5978  1stval2  6243  2ndval2  6244  xp1st  6253  xp2nd  6254  poxp  6320  rntpos  6345  dftpos4  6351  tpostpos  6352  tfrlem7  6405  th3qlem2  6727  ener  6873  domtr  6879  unen  6910  xpsnen  6918  mapen  6945  ltdcnq  7512  archnqq  7532  enq0tr  7549  nqnq0pi  7553  nqnq0  7556  nqpnq0nq  7568  nqnq0a  7569  nqnq0m  7570  nq0m0r  7571  nq0a0  7572  nq02m  7580  prarloc  7618  axaddcl  7979  axmulcl  7981  hashfacen  10983  fundm2domnop0  10992  fsumdvdsmul  15496  bj-inex  15880