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  3582  disjiund  5098  ralxfrd  5363  poxp3  8129  odi  8543  omeulem1  8546  qsss  8749  findcard3  9229  findcard3OLD  9230  ttrclselem2  9679  r1pwss  9737  dfac5lem4  10079  dfac5lem4OLD  10081  climuni  15518  rlimno1  15620  caurcvg2  15644  sscfn1  17779  gsumval2a  18612  gsumval3  19837  opnnei  23007  dislly  23384  lfinpfin  23411  txcmplem1  23528  ufileu  23806  alexsubALT  23938  metustel  24438  metustfbas  24445  i1faddlem  25594  ulmval  26289  brbtwn  28826  vtxduhgr0nedg  29420  wwlksnredwwlkn0  29826  midwwlks2s3  29882  umgr2cycl  35128  iccllysconn  35237  cvmopnlem  35265  cvmlift2lem10  35299  cvmlift3lem8  35313  sdclem2  37736  heibor1lem  37803  elrfi  42682  eldiophb  42745  dnnumch2  43034  inisegn0a  48821