Theorem nex 1729

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

Syntax hints:  ¬ wn 3  ∃wex 1702

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

This theorem depends on definitions:  df-bi 197  df-ex 1703

This theorem is referenced by:  ru  3428  axnulALT  4778  notzfaus  4831  dtrucor2  4892  opelopabsb  4975  0nelxp  5133  0nelxpOLD  5134  0xp  5189  dm0  5328  cnv0  5523  co02  5637  dffv3  6174  mpt20  6710  canth2  8098  brdom3  9335  ruc  14953  meet0  17118  join0  17119  0g0  17244  ustn0  22005  bnj1523  31113  linedegen  32225  nextnt  32379  nextf  32380  unqsym1  32399  amosym1  32400  subsym1  32401  bj-dtrucor2v  32776  bj-ru1  32908  bj-0nelsngl  32934  bj-ccinftydisj  33071