Theorem nexdv 1966

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

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

This theorem is referenced by:  sbc2or  3753  csbopab  5540  csbiota  6529  0mpo0  7493  1sdom2dom  9210  canthwdom  9537  cfsuc  10236  ssfin4  10289  konigthlem  10548  axunndlem1  10575  canthnum  10629  canthwe  10631  pwfseq  10644  tskuni  10763  ptcmplem4  24212  lgsquadlem3  27546  umgredgnlp  29497  iswspthsnon  30205  fineqvinfep  35538  acycgr0v  35640  acycgr2v  35642  prclisacycgr  35643  dfrdg4  36443