Theorem rexlimdvw 3171

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3090

This theorem is used by:  rspcebdv  3573  disjiund  5096  ralxfrd  5373  poxp3  8177  odi  8598  omeulem1  8601  qsss  8807  findcard3  9285  ttrclselem2  9737  r1pwss  9801  dfac5lem4  10215  climuni  15731  rlimno1  15833  caurcvg2  15857  sscfn1  18004  gsumval2a  18886  gsumval3  20133  opnnei  23450  dislly  23828  lfinpfin  23855  txcmplem1  23972  ufileu  24250  alexsubALT  24382  metustel  24881  metustfbas  24888  i1faddlem  26026  ulmval  26719  brbtwn  29489  vtxduhgr0nedg  30085  wwlksnredwwlkn0  30497  midwwlks2s3  30553  umgr2cycl  30759  vonf1oonfo  36003  iccllysconn  36136  cvmopnlem  36164  cvmlift2lem10  36198  cvmlift3lem8  36212  sdclem2  38816  heibor1lem  38883  elrfi  43845  eldiophb  43908  dnnumch2  44192  dmstructnn  46065  dmstructfi  46066  inisegn0a  50086