MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nex Unicode version

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
StepHypRef Expression
1 alnex 1614 . 2
2 nex.1 . 2
31, 2mpgbi 1621 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator