Theorem nexdv 1970

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944

This proof depends on definitions:  df-bi 210  df-ex 1812

This theorem is used by:  sbc2or  3750  csbopab  5533  csbiota  6539  0mpo0  7510  1sdom2dom  9256  canthwdom  9583  cfsuc  10345  ssfin4  10398  konigthlem  10663  axunndlem1  10690  canthnum  10744  canthwe  10746  pwfseq  10759  tskuni  10878  ptcmplem4  24386  lgsquadlem3  27721  umgredgnlp  29737  iswspthsnon  30457  fineqvinfep  35864  acycgr0v  36024  acycgr2v  36026  prclisacycgr  36027  mirimanoffr  36581  dfrdg4  36842