Theorem nex 1795

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

Syntax hints:  ¬ wn 3  ∃wex 1774

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

This theorem depends on definitions:  df-bi 206  df-ex 1775

This theorem is referenced by:  ru  3773  ruOLD  3774  noel  4330  noelOLD  4331  axnulALT  5301  notzfaus  5359  dtrucor2  5368  opelopabsb  5528  0nelopab  5565  0nelxp  5708  0xp  5772  dm0  5919  cnv0  6144  co02  6263  dffv3  6889  mpo0  7502  canth2  9160  snnen2o  9264  1sdom2dom  9274  brdom3  10562  ruc  16240  join0  18425  meet0  18426  0g0  18652  ustn0  24213  bnj1523  34929  linedegen  35980  nexntru  36129  nexfal  36130  unqsym1  36150  bj-dtrucor2v  36535  bj-ru1  36663  bj-0nelsngl  36691  bj-ccinftydisj  36933  disjALTV0  38465  dtrucor3  48222