Theorem exlimdvv 1946

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 1867	. 2 |- ( ph -> ( E. y ps -> ch ) )
3	2	exlimdv 1867	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  4353  opabssxpd  4768  funopg  5367  funopsn  5838  th3qlem1  6849  fundmen  7024  sbthlemi10  7208  addnq0mo  7710  mulnq0mo  7711  genprndl  7784  genprndu  7785  genpdisj  7786  mullocpr  7834  addsrmo  8006  mulsrmo  8007  cnm  8095  summodc  12007  fsum2dlemstep  12058  prodmodc  12202  fprod2dlemstep  12246  txbasval  15061  upgr1een  16048