Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nex | Structured version Visualization version Unicode version |
Description: Generalization rule for negated wff. (Contributed by NM, 18-May-1994.) |
Ref | Expression |
---|---|
nex.1 |
Ref | Expression |
---|---|
nex |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alnex 1706 | . 2 | |
2 | nex.1 | . 2 | |
3 | 1, 2 | mpgbi 1725 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wex 1704 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 |
This theorem depends on definitions: df-bi 197 df-ex 1705 |
This theorem is referenced by: ru 3434 axnulALT 4787 notzfaus 4840 dtrucor2 4901 opelopabsb 4985 0nelxp 5143 0nelxpOLD 5144 0xp 5199 dm0 5339 cnv0 5535 co02 5649 dffv3 6187 mpt20 6725 canth2 8113 brdom3 9350 ruc 14972 meet0 17137 join0 17138 0g0 17263 ustn0 22024 bnj1523 31139 linedegen 32250 nextnt 32404 nextf 32405 unqsym1 32424 amosym1 32425 subsym1 32426 bj-dtrucor2v 32801 bj-ru1 32933 bj-0nelsngl 32959 bj-ccinftydisj 33100 |
Copyright terms: Public domain | W3C validator |