Theorem nex 1882

Description: Generalization rule for negated wff. (Contributed by NM, 18-May-1994.)

Hypothesis

Ref	Expression
nex.1	⊢ ¬ 𝜑

Assertion

Ref	Expression
nex	⊢ ¬ ∃𝑥𝜑

Proof of Theorem nex

Step	Hyp	Ref	Expression
1		alnex 1861	. 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2		nex.1	. 2 ⊢ ¬ 𝜑
3	1, 2	mpgbi 1880	1 ⊢ ¬ ∃𝑥𝜑

Syntax hints:  ¬ wn 3  ∃wex 1859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877

This theorem depends on definitions:  df-bi 198  df-ex 1860

This theorem is referenced by:  ru  3626  axnulALT  4975  notzfaus  5026  dtrucor2  5036  opelopabsb  5174  0nelxp  5338  0xp  5395  dm0  5534  cnv0  5740  co02  5857  dffv3  6398  mpt20  6949  canth2  8346  brdom3  9629  ruc  15186  meet0  17336  join0  17337  0g0  17462  ustn0  22231  bnj1523  31456  linedegen  32565  nextnt  32715  nextf  32716  unqsym1  32735  amosym1  32736  subsym1  32737  bj-dtrucor2v  33109  bj-ru1  33238  bj-0nelsngl  33263  bj-ccinftydisj  33411