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  4252  funopg  5247  th3qlem1  6632  fundmen  6801  sbthlemi10  6960  addnq0mo  7441  mulnq0mo  7442  genprndl  7515  genprndu  7516  genpdisj  7517  mullocpr  7565  addsrmo  7737  mulsrmo  7738  cnm  7826  summodc  11382  fsum2dlemstep  11433  prodmodc  11577  fprod2dlemstep  11621  txbasval  13549