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  4176  copsexg  4362  elopab  4378  epelg  4413  0nelelxp  4780  elvvuni  4816  optocl  4828  xpsspw  4864  relopabi  4882  relop  4907  reldmm  4977  elreldm  4985  xpmlem  5185  dfco2a  5265  unielrel  5292  oprabid  6084  1stval2  6351  2ndval2  6352  xp1st  6361  xp2nd  6362  poxp  6430  rntpos  6490  dftpos4  6496  tpostpos  6497  tfrlem7  6550  th3qlem2  6874  ener  7021  domtr  7027  unen  7060  xpsnen  7074  mapen  7101  ltdcnq  7714  archnqq  7734  enq0tr  7751  nqnq0pi  7755  nqnq0  7758  nqpnq0nq  7770  nqnq0a  7771  nqnq0m  7772  nq0m0r  7773  nq0a0  7774  nq02m  7782  prarloc  7820  axaddcl  8181  axmulcl  8183  hashfacen  11212  fundm2domnop0  11224  fsumdvdsmul  15876  griedg0ssusgr  16263  bj-inex  16694