Theorem rexlimdvw 3218

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  rspcebdv  3545  disjiund  5060  ralxfrd  5326  odi  8372  omeulem1  8375  qsss  8525  findcard3  8987  r1pwss  9473  dfac5lem4  9813  climuni  15189  rlimno1  15293  caurcvg2  15317  sscfn1  17446  gsumval2a  18284  gsumval3  19423  opnnei  22179  dislly  22556  lfinpfin  22583  txcmplem1  22700  ufileu  22978  alexsubALT  23110  metustel  23612  metustfbas  23619  i1faddlem  24762  ulmval  25444  brbtwn  27170  vtxduhgr0nedg  27762  wwlksnredwwlkn0  28162  midwwlks2s3  28218  umgr2cycl  33003  iccllysconn  33112  cvmopnlem  33140  cvmlift2lem10  33174  cvmlift3lem8  33188  ttrclselem2  33712  poxp3  33723  sdclem2  35827  heibor1lem  35894  elrfi  40432  eldiophb  40495  dnnumch2  40786