Theorem exlimivv 1952

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

This proof depends on syntax axioms:   -> wi 4   E.wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1502  ax-ie2 1547  ax-17 1579

This proof depends on definitions:  df-bi 117

This theorem is used by:  cgsex2g  2858  cgsex4g  2859  opabss  4195  copsexg  4384  elopab  4400  epelg  4435  0nelelxp  4803  elvvuni  4839  optocl  4851  xpsspw  4887  relopabi  4905  relop  4930  reldmm  5000  elreldm  5008  xpmlem  5208  dfco2a  5288  unielrel  5315  oprabid  6117  1stval2  6389  2ndval2  6390  xp1st  6399  xp2nd  6400  poxp  6468  rntpos  6528  dftpos4  6534  tpostpos  6535  tfrlem7  6588  th3qlem2  6912  ener  7066  domtr  7072  unen  7105  xpsnen  7119  mapen  7146  ltdcnq  7764  archnqq  7784  enq0tr  7801  nqnq0pi  7805  nqnq0  7808  nqpnq0nq  7820  nqnq0a  7821  nqnq0m  7822  nq0m0r  7823  nq0a0  7824  nq02m  7832  prarloc  7870  axaddcl  8231  axmulcl  8233  hashfacen  11284  fundm2domnop0  11300  fsumdvdsmul  16105  griedg0ssusgr  16492  bj-inex  16933