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  4254  funopg  5250  th3qlem1  6636  fundmen  6805  sbthlemi10  6964  addnq0mo  7445  mulnq0mo  7446  genprndl  7519  genprndu  7520  genpdisj  7521  mullocpr  7569  addsrmo  7741  mulsrmo  7742  cnm  7830  summodc  11390  fsum2dlemstep  11441  prodmodc  11585  fprod2dlemstep  11629  txbasval  13737