Theorem nex 1844

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

Syntax hints:  ¬ wn 3  ∃wex 1823

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

This theorem depends on definitions:  df-bi 199  df-ex 1824

This theorem is referenced by:  ru  3650  noel  4145  axnulALT  5023  notzfaus  5074  dtrucor2  5084  opelopabsb  5222  0nelxp  5389  0xp  5447  dm0  5584  cnv0  5790  co02  5903  dffv3  6442  mpt20  7002  canth2  8401  brdom3  9685  ruc  15376  meet0  17523  join0  17524  0g0  17649  ustn0  22432  bnj1523  31738  linedegen  32839  nexntru  32987  nexfal  32988  unqsym1  33007  amosym1  33008  subsym1  33009  bj-dtrucor2v  33377  bj-ru1  33506  bj-0nelsngl  33531  bj-ccinftydisj  33690  nsb  38102