Theorem nexdv 1938

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

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

This theorem is referenced by:  sbc2or  3738  csbopab  5504  csbiota  6486  0mpo0  7444  1sdom2dom  9158  canthwdom  9488  cfsuc  10173  ssfin4  10226  konigthlem  10485  axunndlem1  10512  canthnum  10566  canthwe  10568  pwfseq  10581  tskuni  10700  ptcmplem4  24033  lgsquadlem3  27362  umgredgnlp  29233  iswspthsnon  29942  fineqvinfep  35288  acycgr0v  35349  acycgr2v  35351  prclisacycgr  35352  dfrdg4  36152