Theorem rexlimdvw 3144

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  rspcebdv  3559  disjiund  5077  ralxfrd  5346  poxp3  8094  odi  8508  omeulem1  8511  qsss  8716  findcard3  9187  ttrclselem2  9641  r1pwss  9702  dfac5lem4  10042  dfac5lem4OLD  10044  climuni  15508  rlimno1  15610  caurcvg2  15634  sscfn1  17778  gsumval2a  18647  gsumval3  19876  opnnei  23098  dislly  23475  lfinpfin  23502  txcmplem1  23619  ufileu  23897  alexsubALT  24029  metustel  24528  metustfbas  24535  i1faddlem  25673  ulmval  26361  brbtwn  28985  vtxduhgr0nedg  29579  wwlksnredwwlkn0  29982  midwwlks2s3  30038  umgr2cycl  35342  iccllysconn  35451  cvmopnlem  35479  cvmlift2lem10  35513  cvmlift3lem8  35527  sdclem2  38080  heibor1lem  38147  elrfi  43143  eldiophb  43206  dnnumch2  43494  inisegn0a  49326