Theorem rexlimdvw 3153

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

Syntax hints:   → wi 4   ∈ wcel 2105  ∃wrex 3070

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 1912

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-rex 3071

This theorem is referenced by:  rspcebdv  3563  disjiund  5076  ralxfrd  5345  odi  8459  omeulem1  8462  qsss  8616  findcard3  9128  findcard3OLD  9129  ttrclselem2  9561  r1pwss  9619  dfac5lem4  9961  climuni  15337  rlimno1  15441  caurcvg2  15465  sscfn1  17603  gsumval2a  18443  gsumval3  19580  opnnei  22351  dislly  22728  lfinpfin  22755  txcmplem1  22872  ufileu  23150  alexsubALT  23282  metustel  23786  metustfbas  23793  i1faddlem  24937  ulmval  25619  brbtwn  27400  vtxduhgr0nedg  27992  wwlksnredwwlkn0  28393  midwwlks2s3  28449  umgr2cycl  33238  iccllysconn  33347  cvmopnlem  33375  cvmlift2lem10  33409  cvmlift3lem8  33423  poxp3  33922  sdclem2  35977  heibor1lem  36044  elrfi  40737  eldiophb  40800  dnnumch2  41092