Theorem nexdv 1936

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  sbc2or  3762  csbopab  5515  relimasn  6056  csbiota  6504  0mpo0  7472  1sdom2dom  9194  canthwdom  9532  cfsuc  10210  ssfin4  10263  konigthlem  10521  axunndlem1  10548  canthnum  10602  canthwe  10604  pwfseq  10617  tskuni  10736  ptcmplem4  23942  lgsquadlem3  27293  umgredgnlp  29074  iswspthsnon  29786  acycgr0v  35135  acycgr2v  35137  prclisacycgr  35138  dfrdg4  35939