Theorem nexdv 1934

Description: Deduction for generalization rule for negated wff. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 13-Jul-2020.) (Proof shortened by Wolf Lammen, 10-Oct-2021.)

Hypothesis

Ref	Expression
nexdv.1	⊢ (𝜑 → ¬ 𝜓)

Assertion

Ref	Expression
nexdv	⊢ (𝜑 → ¬ ∃𝑥𝜓)

Distinct variable group:   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem nexdv

Step	Hyp	Ref	Expression
1		ax-5 1908	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		nexdv.1	. 2 ⊢ (𝜑 → ¬ 𝜓)
3	1, 2	nexdh 1863	1 ⊢ (𝜑 → ¬ ∃𝑥𝜓)

Syntax hints:  ¬ wn 3   → wi 4  ∃wex 1776

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 1908

This theorem depends on definitions:  df-bi 207  df-ex 1777

This theorem is referenced by:  sbc2or  3800  csbopab  5565  relimasn  6105  csbiota  6556  0mpo0  7516  1sdom2dom  9281  canthwdom  9617  cfsuc  10295  ssfin4  10348  konigthlem  10606  axunndlem1  10633  canthnum  10687  canthwe  10689  pwfseq  10702  tskuni  10821  ptcmplem4  24079  lgsquadlem3  27441  umgredgnlp  29179  iswspthsnon  29886  acycgr0v  35133  acycgr2v  35135  prclisacycgr  35136  dfrdg4  35933