Theorem nexdv 1939

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-ex 1782

This theorem is referenced by:  sbc2or  3785  csbopab  5554  relimasn  6080  csbiota  6533  0mpo0  7488  1sdom2dom  9243  canthwdom  9570  cfsuc  10248  ssfin4  10301  konigthlem  10559  axunndlem1  10586  canthnum  10640  canthwe  10642  pwfseq  10655  tskuni  10774  ptcmplem4  23550  lgsquadlem3  26874  umgredgnlp  28396  iswspthsnon  29099  acycgr0v  34127  acycgr2v  34129  prclisacycgr  34130  dfrdg4  34911