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  3572  disjiund  5091  ralxfrd  5355  poxp3  8102  odi  8516  omeulem1  8519  qsss  8724  findcard3  9195  ttrclselem2  9647  r1pwss  9708  dfac5lem4  10048  dfac5lem4OLD  10050  climuni  15487  rlimno1  15589  caurcvg2  15613  sscfn1  17753  gsumval2a  18622  gsumval3  19848  opnnei  23076  dislly  23453  lfinpfin  23480  txcmplem1  23597  ufileu  23875  alexsubALT  24007  metustel  24506  metustfbas  24513  i1faddlem  25662  ulmval  26357  brbtwn  28984  vtxduhgr0nedg  29578  wwlksnredwwlkn0  29981  midwwlks2s3  30037  umgr2cycl  35357  iccllysconn  35466  cvmopnlem  35494  cvmlift2lem10  35528  cvmlift3lem8  35542  sdclem2  37993  heibor1lem  38060  elrfi  43051  eldiophb  43114  dnnumch2  43402  inisegn0a  49195