Theorem exlimdvv 1922

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

Syntax hints:   -> wi 4   E.wex 1516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-5 1471  ax-gen 1473  ax-ie2 1518  ax-17 1550

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  euotd  4317  funopg  5324  funopsn  5785  th3qlem1  6747  fundmen  6922  sbthlemi10  7094  addnq0mo  7595  mulnq0mo  7596  genprndl  7669  genprndu  7670  genpdisj  7671  mullocpr  7719  addsrmo  7891  mulsrmo  7892  cnm  7980  summodc  11809  fsum2dlemstep  11860  prodmodc  12004  fprod2dlemstep  12048  txbasval  14854