Theorem nexdv 1936

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

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

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-ex 1780

This theorem is referenced by:  sbc2or  3779  csbopab  5535  relimasn  6077  csbiota  6529  0mpo0  7495  1sdom2dom  9260  canthwdom  9598  cfsuc  10276  ssfin4  10329  konigthlem  10587  axunndlem1  10614  canthnum  10668  canthwe  10670  pwfseq  10683  tskuni  10802  ptcmplem4  23998  lgsquadlem3  27350  umgredgnlp  29131  iswspthsnon  29843  acycgr0v  35175  acycgr2v  35177  prclisacycgr  35178  dfrdg4  35974