Theorem rexlimdvw 3150

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

Syntax hints:   → wi 4   ∈ wcel 2099  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-rex 3061

This theorem is referenced by:  rspcebdv  3602  disjiund  5143  ralxfrd  5412  poxp3  8164  odi  8609  omeulem1  8612  qsss  8807  findcard3  9319  findcard3OLD  9320  ttrclselem2  9769  r1pwss  9827  dfac5lem4  10169  climuni  15554  rlimno1  15658  caurcvg2  15682  sscfn1  17833  gsumval2a  18678  gsumval3  19905  opnnei  23115  dislly  23492  lfinpfin  23519  txcmplem1  23636  ufileu  23914  alexsubALT  24046  metustel  24550  metustfbas  24557  i1faddlem  25713  ulmval  26409  brbtwn  28833  vtxduhgr0nedg  29429  wwlksnredwwlkn0  29830  midwwlks2s3  29886  umgr2cycl  34969  iccllysconn  35078  cvmopnlem  35106  cvmlift2lem10  35140  cvmlift3lem8  35154  sdclem2  37443  heibor1lem  37510  elrfi  42351  eldiophb  42414  dnnumch2  42706