Theorem exlimivv 1860

Description: Inference form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2080. (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 1858	. 2 |- ( E. y ph -> ps )
3	2	exlimiv 1858	1 |- ( E. x E. y ph -> ps )

Syntax hints:   -> wi 4   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  cgsex2g  3239  cgsex4g  3240  opabss  4714  dtru  4857  copsexg  4956  elopab  4983  elopabr  5013  epelg  5030  0nelelxp  5145  elvvuni  5179  optocl  5195  relopabiALT  5246  relop  5272  elreldm  5350  xpnz  5553  xpdifid  5562  dfco2a  5635  unielrel  5660  unixp0  5669  funsndifnop  6416  fmptsng  6434  oprabid  6677  oprabv  6703  1stval2  7185  2ndval2  7186  1st2val  7194  2nd2val  7195  xp1st  7198  xp2nd  7199  frxp  7287  poxp  7289  soxp  7290  rntpos  7365  dftpos4  7371  tpostpos  7372  wfrlem4  7418  wfrfun  7425  tfrlem7  7479  ener  8002  enerOLD  8003  domtr  8009  unen  8040  xpsnen  8044  sbthlem10  8079  mapen  8124  fseqen  8850  dfac5lem4  8949  kmlem16  8987  axdc4lem  9277  hashfacen  13238  hashle2pr  13259  fundmge2nop0  13274  gictr  17717  dvdsrval  18645  thlle  20041  hmphtr  21586  griedg0ssusgr  26157  rgrusgrprc  26485  numclwlk1lem2fo  27228  frgrregord013  27253  friendship  27257  nvss  27448  spanuni  28403  5oalem7  28519  3oalem3  28523  gsummpt2co  29780  qqhval2  30026  bnj605  30977  bnj607  30986  mppspstlem  31468  mppsval  31469  frrlem4  31783  frrlem5c  31786  pprodss4v  31991  sscoid  32020  colinearex  32167  bj-dtru  32797  stoweidlem35  40252  funop1  41302  sprsymrelfvlem  41740  uspgrsprf  41754  uspgrsprf1  41755