Theorem exlimivv 1948

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

Syntax hints:   -> wi 4   E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1498  ax-ie2 1543  ax-17 1575

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cgsex2g  2852  cgsex4g  2853  opabss  4179  copsexg  4365  elopab  4381  epelg  4416  0nelelxp  4783  elvvuni  4819  optocl  4831  xpsspw  4867  relopabi  4885  relop  4910  reldmm  4980  elreldm  4988  xpmlem  5188  dfco2a  5268  unielrel  5295  oprabid  6090  1stval2  6362  2ndval2  6363  xp1st  6372  xp2nd  6373  poxp  6441  rntpos  6501  dftpos4  6507  tpostpos  6508  tfrlem7  6561  th3qlem2  6885  ener  7032  domtr  7038  unen  7071  xpsnen  7085  mapen  7112  ltdcnq  7728  archnqq  7748  enq0tr  7765  nqnq0pi  7769  nqnq0  7772  nqpnq0nq  7784  nqnq0a  7785  nqnq0m  7786  nq0m0r  7787  nq0a0  7788  nq02m  7796  prarloc  7834  axaddcl  8195  axmulcl  8197  hashfacen  11233  fundm2domnop0  11245  fsumdvdsmul  15985  griedg0ssusgr  16372  bj-inex  16803