Theorem rexlimdvw 3160

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∃wrex 3070

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 3071

This theorem is referenced by:  rspcebdv  3616  disjiund  5134  ralxfrd  5408  poxp3  8175  odi  8617  omeulem1  8620  qsss  8818  findcard3  9318  findcard3OLD  9319  ttrclselem2  9766  r1pwss  9824  dfac5lem4  10166  dfac5lem4OLD  10168  climuni  15588  rlimno1  15690  caurcvg2  15714  sscfn1  17861  gsumval2a  18698  gsumval3  19925  opnnei  23128  dislly  23505  lfinpfin  23532  txcmplem1  23649  ufileu  23927  alexsubALT  24059  metustel  24563  metustfbas  24570  i1faddlem  25728  ulmval  26423  brbtwn  28914  vtxduhgr0nedg  29510  wwlksnredwwlkn0  29916  midwwlks2s3  29972  umgr2cycl  35146  iccllysconn  35255  cvmopnlem  35283  cvmlift2lem10  35317  cvmlift3lem8  35331  sdclem2  37749  heibor1lem  37816  elrfi  42705  eldiophb  42768  dnnumch2  43057