Theorem exlimivv 1943

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

Syntax hints:   -> wi 4   E.wex 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1495  ax-ie2 1540  ax-17 1572

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cgsex2g  2836  cgsex4g  2837  opabss  4148  copsexg  4330  elopab  4346  epelg  4381  0nelelxp  4748  elvvuni  4783  optocl  4795  xpsspw  4831  relopabi  4847  relop  4872  reldmm  4942  elreldm  4950  xpmlem  5149  dfco2a  5229  unielrel  5256  oprabid  6033  1stval2  6301  2ndval2  6302  xp1st  6311  xp2nd  6312  poxp  6378  rntpos  6403  dftpos4  6409  tpostpos  6410  tfrlem7  6463  th3qlem2  6785  ener  6931  domtr  6937  unen  6969  xpsnen  6980  mapen  7007  ltdcnq  7584  archnqq  7604  enq0tr  7621  nqnq0pi  7625  nqnq0  7628  nqpnq0nq  7640  nqnq0a  7641  nqnq0m  7642  nq0m0r  7643  nq0a0  7644  nq02m  7652  prarloc  7690  axaddcl  8051  axmulcl  8053  hashfacen  11058  fundm2domnop0  11067  fsumdvdsmul  15665  bj-inex  16270