Theorem nex 1722

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 1697	. 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2		nex.1	. 2 ⊢ ¬ 𝜑
3	1, 2	mpgbi 1716	1 ⊢ ¬ ∃𝑥𝜑

Syntax hints:  ¬ wn 3  ∃wex 1695

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

This theorem depends on definitions:  df-bi 196  df-ex 1696

This theorem is referenced by:  ru  3401  axnulALT  4715  notzfaus  4766  dtrucor2  4828  opelopabsb  4910  0nelxp  5067  0nelxpOLD  5068  0xp  5122  dm0  5260  cnv0  5454  co02  5566  dffv3  6099  mpt20  6623  canth2  7998  brdom3  9231  ruc  14811  meet0  16960  join0  16961  0g0  17086  ustn0  21834  bnj1523  30393  linedegen  31420  nextnt  31574  nextf  31575  unqsym1  31594  amosym1  31595  subsym1  31596  bj-dtrucor2v  31989  bj-ru1  32125  bj-0nelsngl  32152  bj-ccinftydisj  32277