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  4108  copsexg  4288  elopab  4304  epelg  4337  0nelelxp  4704  elvvuni  4739  optocl  4751  xpsspw  4787  relopabi  4803  relop  4828  elreldm  4904  xpmlem  5103  dfco2a  5183  unielrel  5210  oprabid  5976  1stval2  6241  2ndval2  6242  xp1st  6251  xp2nd  6252  poxp  6318  rntpos  6343  dftpos4  6349  tpostpos  6350  tfrlem7  6403  th3qlem2  6725  ener  6871  domtr  6877  unen  6908  xpsnen  6916  mapen  6943  ltdcnq  7510  archnqq  7530  enq0tr  7547  nqnq0pi  7551  nqnq0  7554  nqpnq0nq  7566  nqnq0a  7567  nqnq0m  7568  nq0m0r  7569  nq0a0  7570  nq02m  7578  prarloc  7616  axaddcl  7977  axmulcl  7979  hashfacen  10981  fundm2domnop0  10990  fsumdvdsmul  15463  bj-inex  15843