Theorem rexlimdvw 3168

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 26	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 3161	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3087

This theorem is used by:  rspcebdv  3570  disjiund  5094  ralxfrd  5373  poxp3  8149  odi  8567  omeulem1  8570  qsss  8776  findcard3  9254  ttrclselem2  9706  r1pwss  9767  dfac5lem4  10130  climuni  15640  rlimno1  15742  caurcvg2  15766  sscfn1  17907  gsumval2a  18788  gsumval3  20035  opnnei  23346  dislly  23724  lfinpfin  23751  txcmplem1  23868  ufileu  24146  alexsubALT  24278  metustel  24777  metustfbas  24784  i1faddlem  25922  ulmval  26617  brbtwn  29357  vtxduhgr0nedg  29953  wwlksnredwwlkn0  30365  midwwlks2s3  30421  umgr2cycl  30627  vonf1oonfo  35713  iccllysconn  35830  cvmopnlem  35858  cvmlift2lem10  35892  cvmlift3lem8  35906  sdclem2  38493  heibor1lem  38560  elrfi  43540  eldiophb  43603  dnnumch2  43887  inisegn0a  49765