Theorem nexdv 1968

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

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

This theorem is used by:  sbc2or  3747  csbopab  5529  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