Theorem nexdv 1943

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  sbc2or  3732  csbopab  5497  csbiota  6478  0mpo0  7439  1sdom2dom  9154  canthwdom  9484  cfsuc  10170  ssfin4  10223  konigthlem  10482  axunndlem1  10509  canthnum  10563  canthwe  10565  pwfseq  10578  tskuni  10697  ptcmplem4  24038  lgsquadlem3  27363  umgredgnlp  29234  iswspthsnon  29942  fineqvinfep  35306  acycgr0v  35376  acycgr2v  35378  prclisacycgr  35379  dfrdg4  36179