Theorem exlimdvv 1895

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

Syntax hints:   -> wi 4   E.wex 1490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1445  ax-gen 1447  ax-ie2 1492  ax-17 1524

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  euotd  4248  funopg  5242  th3qlem1  6627  fundmen  6796  sbthlemi10  6955  addnq0mo  7421  mulnq0mo  7422  genprndl  7495  genprndu  7496  genpdisj  7497  mullocpr  7545  addsrmo  7717  mulsrmo  7718  cnm  7806  summodc  11359  fsum2dlemstep  11410  prodmodc  11554  fprod2dlemstep  11598  txbasval  13347