Theorem nex 1800

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

Syntax hints:  ¬ wn 3  ∃wex 1779

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

This theorem depends on definitions:  df-bi 207  df-ex 1780

This theorem is referenced by:  ru  3748  ruOLD  3749  noel  4297  axnulALT  5254  notzfaus  5313  dtrucor2  5322  opelopabsb  5485  0nelopab  5520  0nelxp  5665  0xp  5729  dm0  5874  cnv0  6101  co02  6221  dffv3  6836  mpo0  7454  canth2  9071  snnen2o  9161  1sdom2dom  9170  brdom3  10457  ruc  16187  join0  18340  meet0  18341  0g0  18567  ustn0  24084  bnj1523  35034  linedegen  36104  nexntru  36365  nexfal  36366  unqsym1  36386  bj-dtrucor2v  36778  bj-ru1  36904  bj-0nelsngl  36932  bj-ccinftydisj  37174  disjALTV0  38719  dtrucor3  48760