Theorem rexlimdvw 3172

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ∃wrex 3090

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 1945

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

This theorem is used by:  rspcebdv  3574  disjiund  5099  ralxfrd  5377  poxp3  8204  odi  8625  omeulem1  8628  qsss  8834  findcard3  9312  ttrclselem2  9764  r1pwss  9828  dfac5lem4  10244  climuni  15763  rlimno1  15865  caurcvg2  15889  sscfn1  18042  gsumval2a  18924  gsumval3  20172  opnnei  23493  dislly  23871  lfinpfin  23898  txcmplem1  24015  ufileu  24293  alexsubALT  24425  metustel  24924  metustfbas  24931  i1faddlem  26069  ulmval  26764  brbtwn  29534  vtxduhgr0nedg  30130  wwlksnredwwlkn0  30542  midwwlks2s3  30598  umgr2cycl  30804  vonf1oonfo  36090  iccllysconn  36223  cvmopnlem  36251  cvmlift2lem10  36285  cvmlift3lem8  36299  sdclem2  38942  heibor1lem  39009  elrfi  43971  eldiophb  44034  dnnumch2  44318  dmstructnn  46188  dmstructfi  46189  inisegn0a  50278