Theorem nexdv 1971

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  sbc2or  3751  csbopab  5537  csbiota  6559  0mpo0  7534  1sdom2dom  9283  canthwdom  9610  cfsuc  10374  ssfin4  10427  konigthlem  10692  axunndlem1  10719  canthnum  10773  canthwe  10775  pwfseq  10788  tskuni  10907  ptcmplem4  24429  lgsquadlem3  27766  umgredgnlp  29782  iswspthsnon  30502  fineqvinfep  35934  acycgr0v  36111  acycgr2v  36113  prclisacycgr  36114  mirimanoffr  36668  dfrdg4  36930