Theorem nexdv 1956

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930

This theorem depends on definitions:  df-bi 209  df-ex 1800

This theorem is referenced by:  sbc2or  3753  csbopab  5526  csbiota  6514  0mpo0  7479  1sdom2dom  9198  canthwdom  9527  cfsuc  10214  ssfin4  10267  konigthlem  10526  axunndlem1  10553  canthnum  10607  canthwe  10609  pwfseq  10622  tskuni  10741  ptcmplem4  24115  lgsquadlem3  27446  umgredgnlp  29348  iswspthsnon  30056  fineqvinfep  35421  acycgr0v  35498  acycgr2v  35500  prclisacycgr  35501  dfrdg4  36301