Theorem rexlimdvw 3169

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∃wrex 3087

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 3088

This theorem is used by:  rspcebdv  3571  disjiund  5094  ralxfrd  5370  poxp3  8167  odi  8587  omeulem1  8590  qsss  8796  findcard3  9274  ttrclselem2  9727  r1pwss  9791  dfac5lem4  10205  climuni  15719  rlimno1  15821  caurcvg2  15845  sscfn1  17992  gsumval2a  18874  gsumval3  20121  opnnei  23438  dislly  23816  lfinpfin  23843  txcmplem1  23960  ufileu  24238  alexsubALT  24370  metustel  24869  metustfbas  24876  i1faddlem  26014  ulmval  26707  brbtwn  29477  vtxduhgr0nedg  30073  wwlksnredwwlkn0  30485  midwwlks2s3  30541  umgr2cycl  30747  vonf1oonfo  35898  iccllysconn  36015  cvmopnlem  36043  cvmlift2lem10  36077  cvmlift3lem8  36091  sdclem2  38676  heibor1lem  38743  elrfi  43704  eldiophb  43767  dnnumch2  44051  dmstructnn  45925  dmstructfi  45926  inisegn0a  49945