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 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1495  ax-gen 1497  ax-ie2 1542  ax-17 1574

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  euotd  4347  opabssxpd  4762  funopg  5360  funopsn  5829  th3qlem1  6805  fundmen  6980  sbthlemi10  7164  addnq0mo  7666  mulnq0mo  7667  genprndl  7740  genprndu  7741  genpdisj  7742  mullocpr  7790  addsrmo  7962  mulsrmo  7963  cnm  8051  summodc  11943  fsum2dlemstep  11994  prodmodc  12138  fprod2dlemstep  12182  txbasval  14990  upgr1een  15974