Theorem nexdv 1937

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  sbc2or  3749  csbopab  5503  csbiota  6485  0mpo0  7441  1sdom2dom  9154  canthwdom  9484  cfsuc  10167  ssfin4  10220  konigthlem  10479  axunndlem1  10506  canthnum  10560  canthwe  10562  pwfseq  10575  tskuni  10694  ptcmplem4  23999  lgsquadlem3  27349  umgredgnlp  29220  iswspthsnon  29929  fineqvinfep  35281  acycgr0v  35342  acycgr2v  35344  prclisacycgr  35345  dfrdg4  36145