Theorem rexlimdvw 3135

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  rspcebdv  3571  disjiund  5083  ralxfrd  5347  poxp3  8083  odi  8497  omeulem1  8500  qsss  8703  findcard3  9172  ttrclselem2  9622  r1pwss  9680  dfac5lem4  10020  dfac5lem4OLD  10022  climuni  15459  rlimno1  15561  caurcvg2  15585  sscfn1  17724  gsumval2a  18559  gsumval3  19786  opnnei  23005  dislly  23382  lfinpfin  23409  txcmplem1  23526  ufileu  23804  alexsubALT  23936  metustel  24436  metustfbas  24443  i1faddlem  25592  ulmval  26287  brbtwn  28844  vtxduhgr0nedg  29438  wwlksnredwwlkn0  29841  midwwlks2s3  29897  umgr2cycl  35124  iccllysconn  35233  cvmopnlem  35261  cvmlift2lem10  35295  cvmlift3lem8  35309  sdclem2  37732  heibor1lem  37799  elrfi  42677  eldiophb  42740  dnnumch2  43028  inisegn0a  48830