Theorem rexlimdvw 3143

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3062

This theorem is referenced by:  rspcebdv  3558  disjiund  5076  ralxfrd  5350  poxp3  8100  odi  8514  omeulem1  8517  qsss  8722  findcard3  9193  ttrclselem2  9647  r1pwss  9708  dfac5lem4  10048  dfac5lem4OLD  10050  climuni  15514  rlimno1  15616  caurcvg2  15640  sscfn1  17784  gsumval2a  18653  gsumval3  19882  opnnei  23085  dislly  23462  lfinpfin  23489  txcmplem1  23606  ufileu  23884  alexsubALT  24016  metustel  24515  metustfbas  24522  i1faddlem  25660  ulmval  26345  brbtwn  28968  vtxduhgr0nedg  29561  wwlksnredwwlkn0  29964  midwwlks2s3  30020  umgr2cycl  35323  iccllysconn  35432  cvmopnlem  35460  cvmlift2lem10  35494  cvmlift3lem8  35508  sdclem2  38063  heibor1lem  38130  elrfi  43126  eldiophb  43189  dnnumch2  43473  inisegn0a  49311