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  3748  csbopab  5534  csbiota  6526  0mpo0  7497  1sdom2dom  9225  canthwdom  9552  cfsuc  10260  ssfin4  10313  konigthlem  10578  axunndlem1  10605  canthnum  10659  canthwe  10661  pwfseq  10674  tskuni  10793  ptcmplem4  24282  lgsquadlem3  27619  umgredgnlp  29605  iswspthsnon  30325  fineqvinfep  35652  acycgr0v  35728  acycgr2v  35730  prclisacycgr  35731  dfrdg4  36531