Theorem rexlimdvw 3170

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 26	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 3163	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃wrex 3088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3089

This theorem is used by:  rspcebdv  3573  disjiund  5098  ralxfrd  5377  poxp3  8152  odi  8570  omeulem1  8573  qsss  8779  findcard3  9257  ttrclselem2  9709  r1pwss  9770  dfac5lem4  10133  climuni  15643  rlimno1  15745  caurcvg2  15769  sscfn1  17912  gsumval2a  18793  gsumval3  20040  opnnei  23351  dislly  23729  lfinpfin  23756  txcmplem1  23873  ufileu  24151  alexsubALT  24283  metustel  24782  metustfbas  24789  i1faddlem  25927  ulmval  26623  brbtwn  29364  vtxduhgr0nedg  29960  wwlksnredwwlkn0  30372  midwwlks2s3  30428  umgr2cycl  30634  vonf1oonfo  35720  iccllysconn  35837  cvmopnlem  35865  cvmlift2lem10  35899  cvmlift3lem8  35913  sdclem2  38500  heibor1lem  38567  elrfi  43547  eldiophb  43610  dnnumch2  43894  inisegn0a  49772