Theorem nexdv 1937

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  sbc2or  3745  csbopab  5493  csbiota  6474  0mpo0  7429  1sdom2dom  9138  canthwdom  9465  cfsuc  10148  ssfin4  10201  konigthlem  10459  axunndlem1  10486  canthnum  10540  canthwe  10542  pwfseq  10555  tskuni  10674  ptcmplem4  23970  lgsquadlem3  27320  umgredgnlp  29125  iswspthsnon  29834  acycgr0v  35192  acycgr2v  35194  prclisacycgr  35195  dfrdg4  35995