Theorem exlimdvv 1869

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

Syntax hints:   -> wi 4   E.wex 1468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1423  ax-gen 1425  ax-ie2 1470  ax-17 1506

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  euotd  4176  funopg  5157  th3qlem1  6531  fundmen  6700  sbthlemi10  6854  addnq0mo  7255  mulnq0mo  7256  genprndl  7329  genprndu  7330  genpdisj  7331  mullocpr  7379  addsrmo  7551  mulsrmo  7552  cnm  7640  summodc  11152  fsum2dlemstep  11203  prodmodc  11347  txbasval  12436