Theorem rexlimdvw 3166

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

Hypothesis

Ref	Expression
rexlimdvw.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
rexlimdvw	⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Distinct variable groups:   𝜑,𝑥   𝜒,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdvw

Step	Hyp	Ref	Expression
1		rexlimdvw.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 3159	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  rspcebdv  3629  disjiund  5157  ralxfrd  5426  poxp3  8191  odi  8635  omeulem1  8638  qsss  8836  findcard3  9346  findcard3OLD  9347  ttrclselem2  9795  r1pwss  9853  dfac5lem4  10195  dfac5lem4OLD  10197  climuni  15598  rlimno1  15702  caurcvg2  15726  sscfn1  17878  gsumval2a  18723  gsumval3  19949  opnnei  23149  dislly  23526  lfinpfin  23553  txcmplem1  23670  ufileu  23948  alexsubALT  24080  metustel  24584  metustfbas  24591  i1faddlem  25747  ulmval  26441  brbtwn  28932  vtxduhgr0nedg  29528  wwlksnredwwlkn0  29929  midwwlks2s3  29985  umgr2cycl  35109  iccllysconn  35218  cvmopnlem  35246  cvmlift2lem10  35280  cvmlift3lem8  35294  sdclem2  37702  heibor1lem  37769  elrfi  42650  eldiophb  42713  dnnumch2  43002