Theorem nexdv 1944

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-ex 1788

This theorem is referenced by:  sbc2or  3692  csbopab  5421  relimasn  5937  csbiota  6351  0mpo0  7272  canthwdom  9173  cfsuc  9836  ssfin4  9889  konigthlem  10147  axunndlem1  10174  canthnum  10228  canthwe  10230  pwfseq  10243  tskuni  10362  ptcmplem4  22906  lgsquadlem3  26217  umgredgnlp  27192  iswspthsnon  27894  acycgr0v  32777  acycgr2v  32779  prclisacycgr  32780  dfrdg4  33939