Theorem rexlimdvw 3034

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

Syntax hints:   → wi 4   ∈ wcel 1990  ∃wrex 2913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-ral 2917  df-rex 2918

This theorem is referenced by:  rspcebdv  3314  disjiund  4643  ralxfrd  4879  odi  7659  omeulem1  7662  qsss  7808  findcard3  8203  r1pwss  8647  dfac5lem4  8949  climuni  14283  rlimno1  14384  caurcvg2  14408  sscfn1  16477  gsumval2a  17279  gsumval3  18308  opnnei  20924  dislly  21300  lfinpfin  21327  txcmplem1  21444  ufileu  21723  alexsubALT  21855  metustel  22355  metustfbas  22362  i1faddlem  23460  ulmval  24134  brbtwn  25779  vtxduhgr0nedg  26388  wwlksnredwwlkn0  26791  elwwlks2ons3  26848  midwwlks2s3  26860  clwwlksnun  26974  iccllysconn  31232  cvmopnlem  31260  cvmlift2lem10  31294  cvmlift3lem8  31308  sdclem2  33538  heibor1lem  33608  elrfi  37257  eldiophb  37320  dnnumch2  37615