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  4283  funopg  5288  th3qlem1  6691  fundmen  6860  sbthlemi10  7025  addnq0mo  7507  mulnq0mo  7508  genprndl  7581  genprndu  7582  genpdisj  7583  mullocpr  7631  addsrmo  7803  mulsrmo  7804  cnm  7892  summodc  11526  fsum2dlemstep  11577  prodmodc  11721  fprod2dlemstep  11765  txbasval  14435