Theorem rexlimdvw 2839

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 18-Jun-2014.)

Hypothesis

Ref	Expression
rexlimdvw.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
rexlimdvw	|- ( ph -> ( E. x e. A ps -> ch ) )

Distinct variable groups:   ph, x   ch, x

Allowed substitution hints:   ps( x)   A( x)

Proof of Theorem rexlimdvw

Step	Hyp	Ref	Expression
1		rexlimdvw.1	. . 3 |- ( ph -> ( ps -> ch ) )
2	1	a1d 25	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	rexlimdv 2835	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   e. wcel 1756   E.wrex 2711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2715  df-rex 2716

This theorem is referenced by:  odi  7010  omeulem1  7013  qsss  7153  findcard3  7547  r1pwss  7983  dfac5lem4  8288  climuni  13022  rlimno1  13123  caurcvg2  13147  sscfn1  14722  gsumval2a  15503  gsumval3OLD  16373  gsumval3  16376  opnnei  18699  dislly  19076  txcmplem1  19189  ufileu  19467  alexsubALT  19598  metustelOLD  20101  metustel  20102  metustfbasOLD  20115  metustfbas  20116  i1faddlem  21146  ulmval  21820  brbtwn  23096  iseupa  23537  iccllyscon  27091  cvmopnlem  27119  cvmlift2lem10  27153  cvmlift3lem8  27167  lfinpfin  28528  sdclem2  28591  heibor1lem  28661  elrfi  28983  eldiophb  29048  dnnumch2  29351  wwlknredwwlkn0  30312  numclwwlkun  30625