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  3579  disjiund  5093  ralxfrd  5358  poxp3  8106  odi  8520  omeulem1  8523  qsss  8726  findcard3  9205  findcard3OLD  9206  ttrclselem2  9655  r1pwss  9713  dfac5lem4  10055  dfac5lem4OLD  10057  climuni  15494  rlimno1  15596  caurcvg2  15620  sscfn1  17759  gsumval2a  18594  gsumval3  19821  opnnei  23040  dislly  23417  lfinpfin  23444  txcmplem1  23561  ufileu  23839  alexsubALT  23971  metustel  24471  metustfbas  24478  i1faddlem  25627  ulmval  26322  brbtwn  28879  vtxduhgr0nedg  29473  wwlksnredwwlkn0  29876  midwwlks2s3  29932  umgr2cycl  35121  iccllysconn  35230  cvmopnlem  35258  cvmlift2lem10  35292  cvmlift3lem8  35306  sdclem2  37729  heibor1lem  37796  elrfi  42675  eldiophb  42738  dnnumch2  43027  inisegn0a  48817