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 ) )

Syntax hints:   -> wi 4   E.wex 1545

This theorem was proved from 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 theorem depends on definitions:  df-bi 117

This theorem is referenced by:  euotd  4390  opabssxpd  4806  funopg  5406  funopsn  5882  th3qlem1  6901  fundmen  7084  sbthlemi10  7273  addnq0mo  7804  mulnq0mo  7805  genprndl  7878  genprndu  7879  genpdisj  7880  mullocpr  7928  addsrmo  8100  mulsrmo  8101  cnm  8189  summodc  12128  fsum2dlemstep  12179  prodmodc  12323  fprod2dlemstep  12367  txbasval  15291  upgr1een  16279