Theorem nexdv 1969

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  sbc2or  3748  csbopab  5530  csbiota  6531  0mpo0  7503  1sdom2dom  9245  canthwdom  9573  cfsuc  10335  ssfin4  10388  konigthlem  10653  axunndlem1  10680  canthnum  10734  canthwe  10736  pwfseq  10749  tskuni  10868  ptcmplem4  24374  lgsquadlem3  27709  umgredgnlp  29725  iswspthsnon  30445  fineqvinfep  35793  acycgr0v  35913  acycgr2v  35915  prclisacycgr  35916  dfrdg4  36715