Theorem rexlimdvw 3063

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

Syntax hints:   → wi 4   ∈ wcel 2030  ∃wrex 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947

This theorem is referenced by:  rspcebdv  3345  disjiund  4675  ralxfrd  4909  odi  7704  omeulem1  7707  qsss  7851  findcard3  8244  r1pwss  8685  dfac5lem4  8987  climuni  14327  rlimno1  14428  caurcvg2  14452  sscfn1  16524  gsumval2a  17326  gsumval3  18354  opnnei  20972  dislly  21348  lfinpfin  21375  txcmplem1  21492  ufileu  21770  alexsubALT  21902  metustel  22402  metustfbas  22409  i1faddlem  23505  ulmval  24179  brbtwn  25824  vtxduhgr0nedg  26444  wwlksnredwwlkn0  26859  midwwlks2s3  26917  elwwlks2ons3OLD  26921  clwwlknunOLD  27091  iccllysconn  31358  cvmopnlem  31386  cvmlift2lem10  31420  cvmlift3lem8  31434  sdclem2  33668  heibor1lem  33738  elrfi  37574  eldiophb  37637  dnnumch2  37932