![]() |
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 1837. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1766 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 1837 | . 2 ⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ Ⅎ𝑥 ¬ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 Ⅎwnf 1765 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 |
This theorem depends on definitions: df-bi 208 df-or 843 df-ex 1762 df-nf 1766 |
This theorem is referenced by: nfnan 1882 nfor 1886 nfa1 2121 nfna1 2122 nfan1 2165 19.32 2200 nfex 2306 cbvexv1 2321 cbvex 2373 cbvex2 2390 nfnae 2413 axc14 2443 euor 2662 euor2 2665 nfne 3087 nfnel 3097 cbvrexf 3398 spcimegf 3532 spcegf 3534 spc2d 3545 cbvrexcsf 3850 nfdif 4023 rabsnifsb 4565 0nelopab 5340 nfpo 5367 nffr 5417 rexxpf 5604 boxcutc 8353 nfoi 8824 rabssnn0fi 13204 fsuppmapnn0fiubex 13210 sumodd 15572 fprodex01 30225 ordtconnlem1 30784 esumrnmpt2 30944 ddemeas 31112 bnj1388 31919 bnj1398 31920 bnj1445 31930 bnj1449 31934 nosupbnd1 32823 nosupbnd2 32825 bj-cbvex2v 33669 finxpreclem6 34208 wl-nfnae1 34301 cdlemefs32sn1aw 37081 ss2iundf 39489 ax6e2ndeqALT 40804 uzwo4 40854 eliin2f 40910 stoweidlem55 41882 stoweidlem59 41886 etransclem32 42093 salexct 42159 sge0f1o 42206 incsmflem 42560 decsmflem 42584 r19.32 42812 |
Copyright terms: Public domain | W3C validator |