Theorem exlimdvv 1953

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

This proof depends on syntax axioms:   -> wi 4   E.wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1500  ax-gen 1502  ax-ie2 1547  ax-17 1579

This proof depends on definitions:  df-bi 117

This theorem is used by:  euotd  4395  opabssxpd  4811  funopg  5411  funopsn  5891  th3qlem1  6911  fundmen  7094  sbthlemi10  7283  addnq0mo  7814  mulnq0mo  7815  genprndl  7888  genprndu  7889  genpdisj  7890  mullocpr  7938  addsrmo  8110  mulsrmo  8111  cnm  8199  summodc  12150  fsum2dlemstep  12201  prodmodc  12345  fprod2dlemstep  12389  txbasval  15368  upgr1een  16365