Theorem nexdv 1940

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

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

This theorem is referenced by:  sbc2or  3787  csbopab  5556  relimasn  6084  csbiota  6537  0mpo0  7492  1sdom2dom  9247  canthwdom  9574  cfsuc  10252  ssfin4  10305  konigthlem  10563  axunndlem1  10590  canthnum  10644  canthwe  10646  pwfseq  10659  tskuni  10778  ptcmplem4  23559  lgsquadlem3  26885  umgredgnlp  28407  iswspthsnon  29110  acycgr0v  34139  acycgr2v  34141  prclisacycgr  34142  dfrdg4  34923