Theorem rexlimdvw 3158

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

Syntax hints:   → wi 4   ∈ wcel 2104  ∃wrex 3068

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 1911

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-rex 3069

This theorem is referenced by:  rspcebdv  3605  disjiund  5137  ralxfrd  5405  poxp3  8138  odi  8581  omeulem1  8584  qsss  8774  findcard3  9287  findcard3OLD  9288  ttrclselem2  9723  r1pwss  9781  dfac5lem4  10123  climuni  15500  rlimno1  15604  caurcvg2  15628  sscfn1  17768  gsumval2a  18610  gsumval3  19816  opnnei  22844  dislly  23221  lfinpfin  23248  txcmplem1  23365  ufileu  23643  alexsubALT  23775  metustel  24279  metustfbas  24286  i1faddlem  25442  ulmval  26128  brbtwn  28424  vtxduhgr0nedg  29016  wwlksnredwwlkn0  29417  midwwlks2s3  29473  umgr2cycl  34430  iccllysconn  34539  cvmopnlem  34567  cvmlift2lem10  34601  cvmlift3lem8  34615  sdclem2  36913  heibor1lem  36980  elrfi  41734  eldiophb  41797  dnnumch2  42089