Theorem rexlimdvw 3209

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

Syntax hints:   → wi 4   ∈ wcel 2110  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-ral 3066  df-rex 3067

This theorem is referenced by:  rspcebdv  3531  disjiund  5043  ralxfrd  5301  odi  8307  omeulem1  8310  qsss  8460  findcard3  8914  r1pwss  9400  dfac5lem4  9740  climuni  15113  rlimno1  15217  caurcvg2  15241  sscfn1  17322  gsumval2a  18157  gsumval3  19292  opnnei  22017  dislly  22394  lfinpfin  22421  txcmplem1  22538  ufileu  22816  alexsubALT  22948  metustel  23448  metustfbas  23455  i1faddlem  24590  ulmval  25272  brbtwn  26990  vtxduhgr0nedg  27580  wwlksnredwwlkn0  27980  midwwlks2s3  28036  umgr2cycl  32816  iccllysconn  32925  cvmopnlem  32953  cvmlift2lem10  32987  cvmlift3lem8  33001  poxp3  33533  sdclem2  35637  heibor1lem  35704  elrfi  40219  eldiophb  40282  dnnumch2  40573