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  3747  csbopab  5501  csbiota  6483  0mpo0  7439  1sdom2dom  9152  canthwdom  9482  cfsuc  10165  ssfin4  10218  konigthlem  10477  axunndlem1  10504  canthnum  10558  canthwe  10560  pwfseq  10573  tskuni  10692  ptcmplem4  23997  lgsquadlem3  27347  umgredgnlp  29169  iswspthsnon  29878  fineqvinfep  35230  acycgr0v  35291  acycgr2v  35293  prclisacycgr  35294  dfrdg4  36094