Theorem rexlimdvw 3142

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

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

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 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3061

This theorem is referenced by:  rspcebdv  3570  disjiund  5089  ralxfrd  5353  poxp3  8092  odi  8506  omeulem1  8509  qsss  8713  findcard3  9183  ttrclselem2  9635  r1pwss  9696  dfac5lem4  10036  dfac5lem4OLD  10038  climuni  15475  rlimno1  15577  caurcvg2  15601  sscfn1  17741  gsumval2a  18610  gsumval3  19836  opnnei  23064  dislly  23441  lfinpfin  23468  txcmplem1  23585  ufileu  23863  alexsubALT  23995  metustel  24494  metustfbas  24501  i1faddlem  25650  ulmval  26345  brbtwn  28972  vtxduhgr0nedg  29566  wwlksnredwwlkn0  29969  midwwlks2s3  30025  umgr2cycl  35335  iccllysconn  35444  cvmopnlem  35472  cvmlift2lem10  35506  cvmlift3lem8  35520  sdclem2  37943  heibor1lem  38010  elrfi  42946  eldiophb  43009  dnnumch2  43297  inisegn0a  49091