Theorem rexlimdvw 3171

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

Syntax hints:   → wi 4   ∈ wcel 2143  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-rex 3090

This theorem is referenced by:  rspcebdv  3575  disjiund  5100  ralxfrd  5379  poxp3  8142  odi  8560  omeulem1  8563  qsss  8769  findcard3  9239  ttrclselem2  9691  r1pwss  9752  dfac5lem4  10106  climuni  15599  rlimno1  15701  caurcvg2  15725  sscfn1  17869  gsumval2a  18738  gsumval3  19972  opnnei  23277  dislly  23654  lfinpfin  23681  txcmplem1  23798  ufileu  24076  alexsubALT  24208  metustel  24707  metustfbas  24714  i1faddlem  25852  ulmval  26543  brbtwn  29249  vtxduhgr0nedg  29842  wwlksnredwwlkn0  30245  midwwlks2s3  30301  vonf1oonfo  35599  umgr2cycl  35633  iccllysconn  35742  cvmopnlem  35770  cvmlift2lem10  35804  cvmlift3lem8  35818  sdclem2  38413  heibor1lem  38480  elrfi  43445  eldiophb  43508  dnnumch2  43792  inisegn0a  49634