Theorem rexlimdvw 2898

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

Syntax hints:   -> wi 4   e. wcel 1842   E.wrex 2754

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-ral 2758  df-rex 2759

This theorem is referenced by:  odi  7185  omeulem1  7188  qsss  7329  findcard3  7717  r1pwss  8154  dfac5lem4  8459  climuni  13431  rlimno1  13532  caurcvg2  13556  sscfn1  15322  gsumval2a  16122  gsumval3OLD  17124  gsumval3  17127  opnnei  19806  dislly  20182  lfinpfin  20209  txcmplem1  20326  ufileu  20604  alexsubALT  20735  metustelOLD  21238  metustel  21239  metustfbasOLD  21252  metustfbas  21253  i1faddlem  22284  ulmval  22959  brbtwn  24500  wwlknredwwlkn0  25025  iseupa  25263  numclwwlkun  25377  iccllyscon  29428  cvmopnlem  29456  cvmlift2lem10  29490  cvmlift3lem8  29504  sdclem2  31498  heibor1lem  31568  elrfi  34969  eldiophb  35032  dnnumch2  35334