Theorem rexlimdvw 3147

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3062

This theorem is referenced by:  rspcebdv  3600  disjiund  5115  ralxfrd  5383  poxp3  8154  odi  8596  omeulem1  8599  qsss  8797  findcard3  9295  findcard3OLD  9296  ttrclselem2  9745  r1pwss  9803  dfac5lem4  10145  dfac5lem4OLD  10147  climuni  15573  rlimno1  15675  caurcvg2  15699  sscfn1  17835  gsumval2a  18668  gsumval3  19893  opnnei  23063  dislly  23440  lfinpfin  23467  txcmplem1  23584  ufileu  23862  alexsubALT  23994  metustel  24494  metustfbas  24501  i1faddlem  25651  ulmval  26346  brbtwn  28883  vtxduhgr0nedg  29477  wwlksnredwwlkn0  29883  midwwlks2s3  29939  umgr2cycl  35168  iccllysconn  35277  cvmopnlem  35305  cvmlift2lem10  35339  cvmlift3lem8  35353  sdclem2  37771  heibor1lem  37838  elrfi  42684  eldiophb  42747  dnnumch2  43036  inisegn0a  48781