Theorem nexdv 1969

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 1943	. 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 1943

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

This theorem is used by:  sbc2or  3755  csbopab  5542  csbiota  6533  0mpo0  7502  1sdom2dom  9221  canthwdom  9548  cfsuc  10256  ssfin4  10309  konigthlem  10570  axunndlem1  10597  canthnum  10651  canthwe  10653  pwfseq  10666  tskuni  10785  ptcmplem4  24265  lgsquadlem3  27599  umgredgnlp  29554  iswspthsnon  30274  fineqvinfep  35597  acycgr0v  35679  acycgr2v  35681  prclisacycgr  35682  dfrdg4  36482