Theorem rexlimdvw 2948

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 2944	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   e. wcel 1758   E.wrex 2799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-ral 2803  df-rex 2804

This theorem is referenced by:  odi  7127  omeulem1  7130  qsss  7270  findcard3  7665  r1pwss  8101  dfac5lem4  8406  climuni  13147  rlimno1  13248  caurcvg2  13272  sscfn1  14848  gsumval2a  15630  gsumval3OLD  16502  gsumval3  16505  opnnei  18855  dislly  19232  txcmplem1  19345  ufileu  19623  alexsubALT  19754  metustelOLD  20257  metustel  20258  metustfbasOLD  20271  metustfbas  20272  i1faddlem  21303  ulmval  21977  brbtwn  23296  iseupa  23737  iccllyscon  27282  cvmopnlem  27310  cvmlift2lem10  27344  cvmlift3lem8  27358  lfinpfin  28722  sdclem2  28785  heibor1lem  28855  elrfi  29177  eldiophb  29242  dnnumch2  29545  wwlknredwwlkn0  30506  numclwwlkun  30819