Theorem exlimdvv 1890

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

Syntax hints:   -> wi 4   E.wex 1485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1440  ax-gen 1442  ax-ie2 1487  ax-17 1519

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  euotd  4239  funopg  5232  th3qlem1  6615  fundmen  6784  sbthlemi10  6943  addnq0mo  7409  mulnq0mo  7410  genprndl  7483  genprndu  7484  genpdisj  7485  mullocpr  7533  addsrmo  7705  mulsrmo  7706  cnm  7794  summodc  11346  fsum2dlemstep  11397  prodmodc  11541  fprod2dlemstep  11585  txbasval  13061