Theorem rexlimdvw 3219

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∃wrex 3065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-ral 3069  df-rex 3070

This theorem is referenced by:  rspcebdv  3555  disjiund  5064  ralxfrd  5331  odi  8410  omeulem1  8413  qsss  8567  findcard3  9057  ttrclselem2  9484  r1pwss  9542  dfac5lem4  9882  climuni  15261  rlimno1  15365  caurcvg2  15389  sscfn1  17529  gsumval2a  18369  gsumval3  19508  opnnei  22271  dislly  22648  lfinpfin  22675  txcmplem1  22792  ufileu  23070  alexsubALT  23202  metustel  23706  metustfbas  23713  i1faddlem  24857  ulmval  25539  brbtwn  27267  vtxduhgr0nedg  27859  wwlksnredwwlkn0  28261  midwwlks2s3  28317  umgr2cycl  33103  iccllysconn  33212  cvmopnlem  33240  cvmlift2lem10  33274  cvmlift3lem8  33288  poxp3  33796  sdclem2  35900  heibor1lem  35967  elrfi  40516  eldiophb  40579  dnnumch2  40870