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  7815  mulnq0mo  7816  genprndl  7889  genprndu  7890  genpdisj  7891  mullocpr  7939  addsrmo  8111  mulsrmo  8112  cnm  8200  summodc  12169  fsum2dlemstep  12220  prodmodc  12364  fprod2dlemstep  12408  txbasval  15459  upgr1een  16531