Theorem nexdv 1938

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  sbc2or  3751  csbopab  5511  csbiota  6493  0mpo0  7451  1sdom2dom  9166  canthwdom  9496  cfsuc  10179  ssfin4  10232  konigthlem  10491  axunndlem1  10518  canthnum  10572  canthwe  10574  pwfseq  10587  tskuni  10706  ptcmplem4  24011  lgsquadlem3  27361  umgredgnlp  29232  iswspthsnon  29941  fineqvinfep  35303  acycgr0v  35364  acycgr2v  35366  prclisacycgr  35367  dfrdg4  36167