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 1847. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1776 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 1847 | . 2 ⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ Ⅎ𝑥 ¬ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 Ⅎwnf 1775 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 |
This theorem depends on definitions: df-bi 208 df-or 842 df-ex 1772 df-nf 1776 |
This theorem is referenced by: nfnan 1892 nfor 1896 nfnaew 2144 nfa1 2146 nfna1 2147 nfan1 2191 19.32 2226 nfex 2335 cbvexv1 2354 cbvex2v 2357 cbvex 2411 cbvex2 2428 nfnae 2451 axc14 2481 euor 2691 euor2 2693 nfne 3119 nfnel 3130 cbvrexfw 3439 cbvrexf 3441 spcimegf 3589 spcegf 3591 spc2d 3602 cbvrexcsf 3925 nfdif 4101 rabsnifsb 4652 0nelopab 5444 nfpo 5473 nffr 5523 rexxpf 5712 boxcutc 8494 nfoi 8967 rabssnn0fi 13344 fsuppmapnn0fiubex 13350 sumodd 15729 fprodex01 30469 ordtconnlem1 31067 esumrnmpt2 31227 ddemeas 31395 bnj1388 32203 bnj1398 32204 bnj1445 32214 bnj1449 32218 nosupbnd1 33112 nosupbnd2 33114 finxpreclem6 34560 wl-nfnae1 34651 cdlemefs32sn1aw 37432 ss2iundf 39884 ax6e2ndeqALT 41145 uzwo4 41195 eliin2f 41251 stoweidlem55 42221 stoweidlem59 42225 etransclem32 42432 salexct 42498 sge0f1o 42545 incsmflem 42899 decsmflem 42923 r19.32 43177 |
Copyright terms: Public domain | W3C validator |