Theorem rexlimdvw 3139

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  rspcebdv  3579  disjiund  5093  ralxfrd  5358  poxp3  8106  odi  8520  omeulem1  8523  qsss  8726  findcard3  9205  findcard3OLD  9206  ttrclselem2  9655  r1pwss  9713  dfac5lem4  10055  dfac5lem4OLD  10057  climuni  15494  rlimno1  15596  caurcvg2  15620  sscfn1  17755  gsumval2a  18588  gsumval3  19813  opnnei  22983  dislly  23360  lfinpfin  23387  txcmplem1  23504  ufileu  23782  alexsubALT  23914  metustel  24414  metustfbas  24421  i1faddlem  25570  ulmval  26265  brbtwn  28802  vtxduhgr0nedg  29396  wwlksnredwwlkn0  29799  midwwlks2s3  29855  umgr2cycl  35101  iccllysconn  35210  cvmopnlem  35238  cvmlift2lem10  35272  cvmlift3lem8  35286  sdclem2  37709  heibor1lem  37776  elrfi  42655  eldiophb  42718  dnnumch2  43007  inisegn0a  48797