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 206  df-ex 1780

This theorem is referenced by:  ru  3720  noel  4270  noelOLD  4271  axnulALT  5237  notzfaus  5294  dtrucor2  5304  opelopabsb  5456  0nelopab  5493  0nelxp  5634  0xp  5696  dm0  5842  cnv0  6059  co02  6178  dffv3  6800  mpo0  7392  canth2  8955  snnen2o  9058  1sdom2dom  9068  brdom3  10334  ruc  16001  join0  18172  meet0  18173  0g0  18397  ustn0  23421  bnj1523  33100  linedegen  34494  nexntru  34642  nexfal  34643  unqsym1  34663  amosym1  34664  subsym1  34665  bj-dtrucor2v  35048  bj-ru1  35180  bj-0nelsngl  35209  bj-ccinftydisj  35432  disjALTV0  36968  dtrucor3  46388