Theorem rexlimdvw 3177

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

Syntax hints:   → wi 4   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-rex 3096

This theorem is referenced by:  rspcebdv  3584  disjiund  5104  ralxfrd  5380  poxp3  8146  odi  8564  omeulem1  8567  qsss  8773  findcard3  9243  ttrclselem2  9695  r1pwss  9756  dfac5lem4  10110  climuni  15603  rlimno1  15705  caurcvg2  15729  sscfn1  17874  gsumval2a  18743  gsumval3  19977  opnnei  23246  dislly  23623  lfinpfin  23650  txcmplem1  23767  ufileu  24045  alexsubALT  24177  metustel  24676  metustfbas  24683  i1faddlem  25821  ulmval  26509  brbtwn  29190  vtxduhgr0nedg  29783  wwlksnredwwlkn0  30186  midwwlks2s3  30242  vonf1oonfo  35498  umgr2cycl  35532  iccllysconn  35641  cvmopnlem  35669  cvmlift2lem10  35703  cvmlift3lem8  35717  sdclem2  38281  heibor1lem  38348  elrfi  43317  eldiophb  43380  dnnumch2  43664  inisegn0a  49499