Theorem nexdv 1935

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

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

This theorem is referenced by:  sbc2or  3813  csbopab  5574  relimasn  6114  csbiota  6566  0mpo0  7533  1sdom2dom  9310  canthwdom  9648  cfsuc  10326  ssfin4  10379  konigthlem  10637  axunndlem1  10664  canthnum  10718  canthwe  10720  pwfseq  10733  tskuni  10852  ptcmplem4  24084  lgsquadlem3  27444  umgredgnlp  29182  iswspthsnon  29889  acycgr0v  35116  acycgr2v  35118  prclisacycgr  35119  dfrdg4  35915