![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfn | Structured version Visualization version GIF version |
Description: Inference associated with nfnt 1953. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1880 changed. (Revised by Wolf Lammen, 18-Sep-2021.) |
Ref | Expression |
---|---|
nfn.1 | ⊢ Ⅎ𝑥𝜑 |
Ref | Expression |
---|---|
nfn | ⊢ Ⅎ𝑥 ¬ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfn.1 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | nfnt 1953 | . 2 ⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ Ⅎ𝑥 ¬ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 Ⅎwnf 1879 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 |
This theorem depends on definitions: df-bi 199 df-or 875 df-ex 1876 df-nf 1880 |
This theorem is referenced by: nfnan 2000 nfor 2004 nfa1 2195 nfna1 2196 nfan1 2232 nfan1OLDOLD 2233 19.32 2268 nfex 2330 cbvexv1 2341 cbvex 2388 cbvex2 2394 nfnae 2418 axc14 2468 sb8vv 2537 euor 2662 euor2 2665 nfne 3069 nfnel 3079 cbvrexf 3347 spcimegf 3473 spcegf 3475 cbvrexcsf 3759 nfdif 3927 rabsnifsb 4444 nfpo 5236 nffr 5284 rexxpf 5471 0neqopab 6930 boxcutc 8189 nfoi 8659 rabssnn0fi 13036 fsuppmapnn0fiubex 13042 sumodd 15444 spc2d 29830 fprodex01 30081 ordtconnlem1 30478 esumrnmpt2 30638 ddemeas 30807 bnj1388 31610 bnj1398 31611 bnj1445 31621 bnj1449 31625 nosupbnd1 32365 nosupbnd2 32367 bj-cbvex2v 33234 finxpreclem6 33723 wl-nfnae1 33798 cdlemefs32sn1aw 36427 ss2iundf 38722 ax6e2ndeqALT 39915 uzwo4 39968 eliin2f 40033 stoweidlem55 41003 stoweidlem59 41007 etransclem32 41214 salexct 41283 sge0f1o 41330 incsmflem 41684 decsmflem 41708 r19.32 41933 |
Copyright terms: Public domain | W3C validator |