Theorem rexlimdvw 3168

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

Syntax hints:   → wi 4   ∈ wcel 2142  ∃wrex 3086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-rex 3087

This theorem is referenced by:  rspcebdv  3575  disjiund  5091  ralxfrd  5365  poxp3  8130  odi  8548  omeulem1  8551  qsss  8757  findcard3  9227  ttrclselem2  9681  r1pwss  9742  dfac5lem4  10082  dfac5lem4OLD  10084  climuni  15579  rlimno1  15681  caurcvg2  15705  sscfn1  17850  gsumval2a  18719  gsumval3  19947  opnnei  23180  dislly  23557  lfinpfin  23584  txcmplem1  23701  ufileu  23979  alexsubALT  24111  metustel  24610  metustfbas  24617  i1faddlem  25755  ulmval  26443  brbtwn  29100  vtxduhgr0nedg  29693  wwlksnredwwlkn0  30096  midwwlks2s3  30152  vonf1oonfo  35458  umgr2cycl  35491  iccllysconn  35600  cvmopnlem  35628  cvmlift2lem10  35662  cvmlift3lem8  35676  sdclem2  38241  heibor1lem  38308  elrfi  43275  eldiophb  43338  dnnumch2  43622  inisegn0a  49457