Theorem rexlimdvw 3145

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

Syntax hints:   → wi 4   ∈ wcel 2119  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3064

This theorem is referenced by:  rspcebdv  3554  disjiund  5063  ralxfrd  5337  poxp3  8090  odi  8504  omeulem1  8507  qsss  8712  findcard3  9183  ttrclselem2  9638  r1pwss  9699  dfac5lem4  10039  dfac5lem4OLD  10041  climuni  15505  rlimno1  15607  caurcvg2  15631  sscfn1  17775  gsumval2a  18644  gsumval3  19873  opnnei  23103  dislly  23480  lfinpfin  23507  txcmplem1  23624  ufileu  23902  alexsubALT  24034  metustel  24533  metustfbas  24540  i1faddlem  25678  ulmval  26363  brbtwn  28986  vtxduhgr0nedg  29579  wwlksnredwwlkn0  29982  midwwlks2s3  30038  umgr2cycl  35369  iccllysconn  35478  cvmopnlem  35506  cvmlift2lem10  35540  cvmlift3lem8  35554  sdclem2  38109  heibor1lem  38176  elrfi  43143  eldiophb  43206  dnnumch2  43490  inisegn0a  49326