Theorem nexdv 1935

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 1909	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
2		nexdv.1	. 2 ⊢ (𝜑 → ¬ 𝜓)
3	1, 2	nexdh 1864	1 ⊢ (𝜑 → ¬ ∃𝑥𝜓)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

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

This theorem is referenced by:  sbc2or  3796  csbopab  5559  relimasn  6102  csbiota  6553  0mpo0  7517  1sdom2dom  9284  canthwdom  9620  cfsuc  10298  ssfin4  10351  konigthlem  10609  axunndlem1  10636  canthnum  10690  canthwe  10692  pwfseq  10705  tskuni  10824  ptcmplem4  24064  lgsquadlem3  27427  umgredgnlp  29165  iswspthsnon  29877  acycgr0v  35154  acycgr2v  35156  prclisacycgr  35157  dfrdg4  35953