Theorem rexlimdvw 3290

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

Syntax hints:   → wi 4   ∈ wcel 2110  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-ral 3143  df-rex 3144

This theorem is referenced by:  rspcebdv  3617  disjiund  5049  ralxfrd  5301  odi  8199  omeulem1  8202  qsss  8352  findcard3  8755  r1pwss  9207  dfac5lem4  9546  climuni  14903  rlimno1  15004  caurcvg2  15028  sscfn1  17081  gsumval2a  17889  gsumval3  19021  opnnei  21722  dislly  22099  lfinpfin  22126  txcmplem1  22243  ufileu  22521  alexsubALT  22653  metustel  23154  metustfbas  23161  i1faddlem  24288  ulmval  24962  brbtwn  26679  vtxduhgr0nedg  27268  wwlksnredwwlkn0  27668  midwwlks2s3  27725  umgr2cycl  32383  iccllysconn  32492  cvmopnlem  32520  cvmlift2lem10  32554  cvmlift3lem8  32568  sdclem2  35011  heibor1lem  35081  elrfi  39284  eldiophb  39347  dnnumch2  39638