Theorem rexlimdvw 3161

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∃wrex 3071

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 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  rspcebdv  3607  disjiund  5139  ralxfrd  5407  poxp3  8136  odi  8579  omeulem1  8582  qsss  8772  findcard3  9285  findcard3OLD  9286  ttrclselem2  9721  r1pwss  9779  dfac5lem4  10121  climuni  15496  rlimno1  15600  caurcvg2  15624  sscfn1  17764  gsumval2a  18604  gsumval3  19775  opnnei  22624  dislly  23001  lfinpfin  23028  txcmplem1  23145  ufileu  23423  alexsubALT  23555  metustel  24059  metustfbas  24066  i1faddlem  25210  ulmval  25892  brbtwn  28157  vtxduhgr0nedg  28749  wwlksnredwwlkn0  29150  midwwlks2s3  29206  umgr2cycl  34132  iccllysconn  34241  cvmopnlem  34269  cvmlift2lem10  34303  cvmlift3lem8  34317  sdclem2  36610  heibor1lem  36677  elrfi  41432  eldiophb  41495  dnnumch2  41787