Theorem exlimdvv 1870

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

Syntax hints:   -> wi 4   E.wex 1469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1424  ax-gen 1426  ax-ie2 1471  ax-17 1507

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  euotd  4184  funopg  5165  th3qlem1  6539  fundmen  6708  sbthlemi10  6862  addnq0mo  7279  mulnq0mo  7280  genprndl  7353  genprndu  7354  genpdisj  7355  mullocpr  7403  addsrmo  7575  mulsrmo  7576  cnm  7664  summodc  11184  fsum2dlemstep  11235  prodmodc  11379  txbasval  12475