Theorem exlimdvv 1862

Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2080. (Contributed by NM, 31-Jul-1995.)

Hypothesis

Ref	Expression
exlimdvv.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
exlimdvv	|- ( ph -> ( E. x E. y ps -> ch ) )

Distinct variable groups:   ch, x   ph, x   ch, y   ph, y

Allowed substitution hints:   ps( x, y)

Proof of Theorem exlimdvv

Step	Hyp	Ref	Expression
1		exlimdvv.1	. . 3 |- ( ph -> ( ps -> ch ) )
2	1	exlimdv 1861	. 2 |- ( ph -> ( E. y ps -> ch ) )
3	2	exlimdv 1861	1 |- ( ph -> ( E. x E. y ps -> ch ) )

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:  euotd  4975  opabssxpd  5338  funopg  5922  fmptsnd  6435  tpres  6466  fundmen  8030  undom  8048  infxpenc2  8845  zorn2lem6  9323  fpwwe2lem12  9463  genpnnp  9827  addsrmo  9894  mulsrmo  9895  hashfun  13224  hash2exprb  13253  rtrclreclem3  13800  summo  14448  fsum2dlem  14501  ntrivcvgmul  14634  prodmo  14666  fprod2dlem  14710  iscatd2  16342  gsumval3eu  18305  gsum2d2  18373  ptbasin  21380  txcls  21407  txbasval  21409  reconn  22631  phtpcer  22794  phtpcerOLD  22795  pcohtpy  22820  mbfi1flimlem  23489  mbfmullem  23492  itg2add  23526  fsumvma  24938  umgr3v3e3cycl  27044  conngrv2edg  27055  pconnconn  31213  txsconn  31223  dfpo2  31645  neibastop1  32354  itg2addnc  33464  riscer  33787  dalem62  35020  pellexlem5  37397  pellex  37399  iunrelexpuztr  38011  fzisoeu  39514  stoweidlem53  40270  stoweidlem56  40273