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  6916  fundmen  7100  sbthlemi10  7290  addnq0mo  7820  mulnq0mo  7821  genprndl  7894  genprndu  7895  genpdisj  7896  mullocpr  7944  addsrmo  8116  mulsrmo  8117  cnm  8205  summodc  12174  fsum2dlemstep  12225  prodmodc  12369  fprod2dlemstep  12413  gsum2d2fi  14273  txbasval  15510  upgr1een  16587