Theorem exlimdvv 1909

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

Syntax hints:   -> wi 4   E.wex 1503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1458  ax-gen 1460  ax-ie2 1505  ax-17 1537

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  euotd  4284  funopg  5289  th3qlem1  6693  fundmen  6862  sbthlemi10  7027  addnq0mo  7509  mulnq0mo  7510  genprndl  7583  genprndu  7584  genpdisj  7585  mullocpr  7633  addsrmo  7805  mulsrmo  7806  cnm  7894  summodc  11529  fsum2dlemstep  11580  prodmodc  11724  fprod2dlemstep  11768  txbasval  14446