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  3737  csbopab  5510  csbiota  6491  0mpo0  7450  1sdom2dom  9164  canthwdom  9494  cfsuc  10179  ssfin4  10232  konigthlem  10491  axunndlem1  10518  canthnum  10572  canthwe  10574  pwfseq  10587  tskuni  10706  ptcmplem4  24020  lgsquadlem3  27345  umgredgnlp  29216  iswspthsnon  29924  fineqvinfep  35269  acycgr0v  35330  acycgr2v  35332  prclisacycgr  35333  dfrdg4  36133