Theorem exlimivv 1896

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

Syntax hints:   -> wi 4   E.wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1449  ax-ie2 1494  ax-17 1526

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cgsex2g  2775  cgsex4g  2776  opabss  4069  copsexg  4246  elopab  4260  epelg  4292  0nelelxp  4657  elvvuni  4692  optocl  4704  xpsspw  4740  relopabi  4754  relop  4779  elreldm  4855  xpmlem  5051  dfco2a  5131  unielrel  5158  oprabid  5909  1stval2  6158  2ndval2  6159  xp1st  6168  xp2nd  6169  poxp  6235  rntpos  6260  dftpos4  6266  tpostpos  6267  tfrlem7  6320  th3qlem2  6640  ener  6781  domtr  6787  unen  6818  xpsnen  6823  mapen  6848  ltdcnq  7398  archnqq  7418  enq0tr  7435  nqnq0pi  7439  nqnq0  7442  nqpnq0nq  7454  nqnq0a  7455  nqnq0m  7456  nq0m0r  7457  nq0a0  7458  nq02m  7466  prarloc  7504  axaddcl  7865  axmulcl  7867  hashfacen  10818  bj-inex  14698