Theorem rexlimdvw 3138

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∃wrex 3056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3057

This theorem is referenced by:  rspcebdv  3566  disjiund  5080  ralxfrd  5344  poxp3  8080  odi  8494  omeulem1  8497  qsss  8700  findcard3  9167  ttrclselem2  9616  r1pwss  9677  dfac5lem4  10017  dfac5lem4OLD  10019  climuni  15459  rlimno1  15561  caurcvg2  15585  sscfn1  17724  gsumval2a  18593  gsumval3  19819  opnnei  23035  dislly  23412  lfinpfin  23439  txcmplem1  23556  ufileu  23834  alexsubALT  23966  metustel  24465  metustfbas  24472  i1faddlem  25621  ulmval  26316  brbtwn  28877  vtxduhgr0nedg  29471  wwlksnredwwlkn0  29874  midwwlks2s3  29930  umgr2cycl  35185  iccllysconn  35294  cvmopnlem  35322  cvmlift2lem10  35356  cvmlift3lem8  35370  sdclem2  37792  heibor1lem  37859  elrfi  42797  eldiophb  42860  dnnumch2  43148  inisegn0a  48946