Theorem rexlimdvw 3140

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 3133	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

Syntax hints:   → wi 4   ∈ wcel 2113  ∃wrex 3058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3059

This theorem is referenced by:  rspcebdv  3568  disjiund  5087  ralxfrd  5351  poxp3  8090  odi  8504  omeulem1  8507  qsss  8711  findcard3  9181  ttrclselem2  9633  r1pwss  9694  dfac5lem4  10034  dfac5lem4OLD  10036  climuni  15473  rlimno1  15575  caurcvg2  15599  sscfn1  17739  gsumval2a  18608  gsumval3  19834  opnnei  23062  dislly  23439  lfinpfin  23466  txcmplem1  23583  ufileu  23861  alexsubALT  23993  metustel  24492  metustfbas  24499  i1faddlem  25648  ulmval  26343  brbtwn  28921  vtxduhgr0nedg  29515  wwlksnredwwlkn0  29918  midwwlks2s3  29974  umgr2cycl  35284  iccllysconn  35393  cvmopnlem  35421  cvmlift2lem10  35455  cvmlift3lem8  35469  sdclem2  37882  heibor1lem  37949  elrfi  42878  eldiophb  42941  dnnumch2  43229  inisegn0a  49023