Theorem exlimivv 1825

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

Syntax hints:   -> wi 4   E.wex 1427

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-gen 1384  ax-ie2 1429  ax-17 1465

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  cgsex2g  2656  cgsex4g  2657  opabss  3908  copsexg  4080  elopab  4094  epelg  4126  0nelelxp  4480  elvvuni  4515  optocl  4527  xpsspw  4563  relopabi  4576  relop  4599  elreldm  4674  xpmlem  4865  dfco2a  4944  unielrel  4971  oprabid  5695  1stval2  5940  2ndval2  5941  xp1st  5950  xp2nd  5951  poxp  6011  rntpos  6036  dftpos4  6042  tpostpos  6043  tfrlem7  6096  th3qlem2  6409  ener  6550  domtr  6556  unen  6587  xpsnen  6591  mapen  6616  ltdcnq  7017  archnqq  7037  enq0tr  7054  nqnq0pi  7058  nqnq0  7061  nqpnq0nq  7073  nqnq0a  7074  nqnq0m  7075  nq0m0r  7076  nq0a0  7077  nq02m  7085  prarloc  7123  axaddcl  7462  axmulcl  7464  hashfacen  10302  bj-inex  12071