Theorem exlimdvv 1921

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

Syntax hints:   -> wi 4   E.wex 1515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1470  ax-gen 1472  ax-ie2 1517  ax-17 1549

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  euotd  4299  funopg  5305  funopsn  5762  th3qlem1  6724  fundmen  6898  sbthlemi10  7068  addnq0mo  7560  mulnq0mo  7561  genprndl  7634  genprndu  7635  genpdisj  7636  mullocpr  7684  addsrmo  7856  mulsrmo  7857  cnm  7945  summodc  11694  fsum2dlemstep  11745  prodmodc  11889  fprod2dlemstep  11933  txbasval  14739