Theorem exlimdvv 1897

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 1819	. 2 |- ( ph -> ( E. y ps -> ch ) )
3	2	exlimdv 1819	1 |- ( ph -> ( E. x E. y ps -> ch ) )

Syntax hints:   -> wi 4   E.wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1447  ax-gen 1449  ax-ie2 1494  ax-17 1526

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  euotd  4255  funopg  5251  th3qlem1  6637  fundmen  6806  sbthlemi10  6965  addnq0mo  7446  mulnq0mo  7447  genprndl  7520  genprndu  7521  genpdisj  7522  mullocpr  7570  addsrmo  7742  mulsrmo  7743  cnm  7831  summodc  11391  fsum2dlemstep  11442  prodmodc  11586  fprod2dlemstep  11630  txbasval  13770