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  3751  csbopab  5498  relimasn  6036  csbiota  6475  0mpo0  7432  1sdom2dom  9143  canthwdom  9471  cfsuc  10151  ssfin4  10204  konigthlem  10462  axunndlem1  10489  canthnum  10543  canthwe  10545  pwfseq  10558  tskuni  10677  ptcmplem4  23940  lgsquadlem3  27291  umgredgnlp  29092  iswspthsnon  29801  acycgr0v  35125  acycgr2v  35127  prclisacycgr  35128  dfrdg4  35929