Theorem exlimdvv 1920

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

Syntax hints:   -> wi 4   E.wex 1514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1469  ax-gen 1471  ax-ie2 1516  ax-17 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  euotd  4298  funopg  5304  funopsn  5761  th3qlem1  6723  fundmen  6897  sbthlemi10  7067  addnq0mo  7559  mulnq0mo  7560  genprndl  7633  genprndu  7634  genpdisj  7635  mullocpr  7683  addsrmo  7855  mulsrmo  7856  cnm  7944  summodc  11665  fsum2dlemstep  11716  prodmodc  11860  fprod2dlemstep  11904  txbasval  14710