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

Theorem nex 1565
 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 1553 . 2
2 nex.1 . 2
31, 2mpgbi 1559 1
 Colors of variables: wff set class Syntax hints:   wn 3  wex 1551 This theorem is referenced by:  ru  3162  axnulALT  4339  notzfaus  4377  dtrucor2  4401  opelopabsb  4468  0nelxp  4909  xp0r  4959  dm0  5086  co02  5386  dffv3  5727  mpt20  6430  canth2  7263  brdom3  8411  ruc  12847  0g0  14714  ustn0  18255  linedegen  26082  nextnt  26160  nextf  26161  unqsym1  26180  amosym1  26181  subsym1  26182  bnj1523  29514 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556 This theorem depends on definitions:  df-bi 179  df-ex 1552
 Copyright terms: Public domain W3C validator