Theorem nexdv 1936

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  sbc2or  3759  csbopab  5510  relimasn  6045  csbiota  6492  0mpo0  7452  1sdom2dom  9170  canthwdom  9508  cfsuc  10186  ssfin4  10239  konigthlem  10497  axunndlem1  10524  canthnum  10578  canthwe  10580  pwfseq  10593  tskuni  10712  ptcmplem4  23918  lgsquadlem3  27269  umgredgnlp  29050  iswspthsnon  29759  acycgr0v  35108  acycgr2v  35110  prclisacycgr  35111  dfrdg4  35912