Theorem exlimivv 1921

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

Syntax hints:   -> wi 4   E.wex 1516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1473  ax-ie2 1518  ax-17 1550

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  cgsex2g  2813  cgsex4g  2814  opabss  4124  copsexg  4306  elopab  4322  epelg  4355  0nelelxp  4722  elvvuni  4757  optocl  4769  xpsspw  4805  relopabi  4821  relop  4846  elreldm  4923  xpmlem  5122  dfco2a  5202  unielrel  5229  oprabid  5999  1stval2  6264  2ndval2  6265  xp1st  6274  xp2nd  6275  poxp  6341  rntpos  6366  dftpos4  6372  tpostpos  6373  tfrlem7  6426  th3qlem2  6748  ener  6894  domtr  6900  unen  6932  xpsnen  6941  mapen  6968  ltdcnq  7545  archnqq  7565  enq0tr  7582  nqnq0pi  7586  nqnq0  7589  nqpnq0nq  7601  nqnq0a  7602  nqnq0m  7603  nq0m0r  7604  nq0a0  7605  nq02m  7613  prarloc  7651  axaddcl  8012  axmulcl  8014  hashfacen  11018  fundm2domnop0  11027  fsumdvdsmul  15578  bj-inex  16042