Theorem rexlimdvw 3173

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 26	. 2 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝜓 → 𝜒)))
3	2	rexlimdv 3166	1 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ∃wrex 3091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3092

This theorem is used by:  rspcebdv  3577  disjiund  5102  ralxfrd  5381  poxp3  8152  odi  8570  omeulem1  8573  qsss  8779  findcard3  9250  ttrclselem2  9702  r1pwss  9763  dfac5lem4  10126  climuni  15629  rlimno1  15731  caurcvg2  15755  sscfn1  17898  gsumval2a  18777  gsumval3  20023  opnnei  23329  dislly  23707  lfinpfin  23734  txcmplem1  23851  ufileu  24129  alexsubALT  24261  metustel  24760  metustfbas  24767  i1faddlem  25905  ulmval  26596  brbtwn  29306  vtxduhgr0nedg  29902  wwlksnredwwlkn0  30314  midwwlks2s3  30370  umgr2cycl  30576  vonf1oonfo  35658  iccllysconn  35781  cvmopnlem  35809  cvmlift2lem10  35843  cvmlift3lem8  35857  sdclem2  38453  heibor1lem  38520  elrfi  43485  eldiophb  43548  dnnumch2  43832  inisegn0a  49673