Theorem nexdv 1963

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-ex 1807

This theorem is referenced by:  sbc2or  3762  csbopab  5541  csbiota  6530  0mpo0  7494  1sdom2dom  9214  canthwdom  9541  cfsuc  10241  ssfin4  10294  konigthlem  10553  axunndlem1  10580  canthnum  10634  canthwe  10636  pwfseq  10649  tskuni  10768  ptcmplem4  24181  lgsquadlem3  27512  umgredgnlp  29438  iswspthsnon  30146  fineqvinfep  35461  acycgr0v  35539  acycgr2v  35541  prclisacycgr  35542  dfrdg4  36342