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  4397  opabssxpd  4813  funopg  5414  funopsn  5894  th3qlem1  6915  fundmen  7098  sbthlemi10  7288  addnq0mo  7820  mulnq0mo  7821  genprndl  7894  genprndu  7895  genpdisj  7896  mullocpr  7944  addsrmo  8116  mulsrmo  8117  cnm  8205  summodc  12175  fsum2dlemstep  12226  prodmodc  12370  fprod2dlemstep  12414  gsum2d2fi  14274  txbasval  15493  upgr1een  16570