Theorem nexdv 1932

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-ex 1775

This theorem is referenced by:  sbc2or  3785  csbopab  5561  relimasn  6094  csbiota  6547  0mpo0  7508  1sdom2dom  9281  canthwdom  9622  cfsuc  10300  ssfin4  10353  konigthlem  10611  axunndlem1  10638  canthnum  10692  canthwe  10694  pwfseq  10707  tskuni  10826  ptcmplem4  24050  lgsquadlem3  27411  umgredgnlp  29083  iswspthsnon  29790  acycgr0v  34976  acycgr2v  34978  prclisacycgr  34979  dfrdg4  35775