Theorem rexlimdvw 2882

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 26	. 2 |- ( ph -> ( x e. A -> ( ps -> ch ) ) )
3	2	rexlimdv 2877	1 |- ( ph -> ( E. x e. A ps -> ch ) )

Syntax hints:   -> wi 4   e. wcel 1887   E.wrex 2738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-ral 2742  df-rex 2743

This theorem is referenced by:  odi  7280  omeulem1  7283  qsss  7424  findcard3  7814  r1pwss  8255  dfac5lem4  8557  climuni  13616  rlimno1  13717  caurcvg2  13744  sscfn1  15722  gsumval2a  16522  gsumval3  17541  opnnei  20136  dislly  20512  lfinpfin  20539  txcmplem1  20656  ufileu  20934  alexsubALT  21066  metustel  21565  metustfbas  21572  i1faddlem  22651  ulmval  23335  brbtwn  24929  wwlknredwwlkn0  25455  iseupa  25693  numclwwlkun  25807  iccllyscon  29973  cvmopnlem  30001  cvmlift2lem10  30035  cvmlift3lem8  30049  sdclem2  32071  heibor1lem  32141  elrfi  35536  eldiophb  35599  dnnumch2  35903  vtxduhgr0nedg  39546