Theorem exlimdvv 1885

Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (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 1807	. 2 |- ( ph -> ( E. y ps -> ch ) )
3	2	exlimdv 1807	1 |- ( ph -> ( E. x E. y ps -> ch ) )

Syntax hints:   -> wi 4   E.wex 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1435  ax-gen 1437  ax-ie2 1482  ax-17 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  euotd  4232  funopg  5222  th3qlem1  6603  fundmen  6772  sbthlemi10  6931  addnq0mo  7388  mulnq0mo  7389  genprndl  7462  genprndu  7463  genpdisj  7464  mullocpr  7512  addsrmo  7684  mulsrmo  7685  cnm  7773  summodc  11324  fsum2dlemstep  11375  prodmodc  11519  fprod2dlemstep  11563  txbasval  12907