Theorem rexlimdvw 3157

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

Syntax hints:   → wi 4   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  rspcebdv  3615  disjiund  5138  ralxfrd  5413  poxp3  8173  odi  8615  omeulem1  8618  qsss  8816  findcard3  9315  findcard3OLD  9316  ttrclselem2  9763  r1pwss  9821  dfac5lem4  10163  dfac5lem4OLD  10165  climuni  15584  rlimno1  15686  caurcvg2  15710  sscfn1  17864  gsumval2a  18710  gsumval3  19939  opnnei  23143  dislly  23520  lfinpfin  23547  txcmplem1  23664  ufileu  23942  alexsubALT  24074  metustel  24578  metustfbas  24585  i1faddlem  25741  ulmval  26437  brbtwn  28928  vtxduhgr0nedg  29524  wwlksnredwwlkn0  29925  midwwlks2s3  29981  umgr2cycl  35125  iccllysconn  35234  cvmopnlem  35262  cvmlift2lem10  35296  cvmlift3lem8  35310  sdclem2  37728  heibor1lem  37795  elrfi  42681  eldiophb  42744  dnnumch2  43033