Theorem rexlimdvw 3182

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991

This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-ral 3066  df-rex 3067

This theorem is referenced by:  rspcebdv  3465  disjiund  4777  ralxfrd  5008  odi  7811  omeulem1  7814  qsss  7958  findcard3  8357  r1pwss  8809  dfac5lem4  9147  climuni  14484  rlimno1  14585  caurcvg2  14609  sscfn1  16677  gsumval2a  17480  gsumval3  18508  opnnei  21138  dislly  21514  lfinpfin  21541  txcmplem1  21658  ufileu  21936  alexsubALT  22068  metustel  22568  metustfbas  22575  i1faddlem  23673  ulmval  24347  brbtwn  25993  vtxduhgr0nedg  26616  wwlksnredwwlkn0  27033  midwwlks2s3  27092  elwwlks2ons3OLD  27096  clwwlknunOLD  27286  iccllysconn  31563  cvmopnlem  31591  cvmlift2lem10  31625  cvmlift3lem8  31639  sdclem2  33863  heibor1lem  33933  elrfi  37776  eldiophb  37839  dnnumch2  38134