Theorem nex 1627

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 1614	. 2
2		nex.1	. 2
3	1, 2	mpgbi 1621	1

Syntax hints:  -.wn 3  E.wex 1612

This theorem is referenced by:  ru  3326  axnulALT  4579  notzfaus  4627  dtrucor2  4686  opelopabsb  4762  0nelxp  5032  0xp  5085  dm0  5221  co02  5526  dffv3  5867  mpt20  6367  canth2  7690  brdom3  8927  ruc  13976  meet0  15767  join0  15768  0g0  15890  ustn0  20723  linedegen  29793  nextnt  29870  nextf  29871  unqsym1  29890  amosym1  29891  subsym1  29892  bnj1523  34127  bj-dtrucor2v  34387  bj-ru1  34501  bj-0nelsngl  34529  bj-ccinftydisj  34616

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

This theorem depends on definitions:  df-bi 185  df-ex 1613