Theorem exlimdvv 1947

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

Syntax hints:   -> wi 4   E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1496  ax-gen 1498  ax-ie2 1543  ax-17 1575

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  euotd  4371  opabssxpd  4786  funopg  5386  funopsn  5860  th3qlem1  6871  fundmen  7047  sbthlemi10  7236  addnq0mo  7762  mulnq0mo  7763  genprndl  7836  genprndu  7837  genpdisj  7838  mullocpr  7886  addsrmo  8058  mulsrmo  8059  cnm  8147  summodc  12069  fsum2dlemstep  12120  prodmodc  12264  fprod2dlemstep  12308  txbasval  15132  upgr1een  16119