| 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 1889. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1817 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 1889 | . 2 ⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ Ⅎ𝑥 ¬ 𝜑 |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: ¬ wn 3 Ⅎwnf 1816 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 |
| This proof depends on definitions: df-bi 210 df-or 862 df-ex 1813 df-nf 1817 |
| This theorem is used by: nfnan 1933 nfor 1937 nfa1 2189 nfna1 2190 nfan1 2239 19.32 2272 nfex 2359 cbvexv1 2376 cbvex2v 2378 cbvex 2433 cbvex2 2446 nfnae 2468 axc14 2497 euor 2641 euor2 2643 nfne 3063 nfnel 3074 cbvrexfw 3308 cbvrexf 3352 ceqsex 3504 spcimegf 3521 spcegf 3553 spc2d 3563 cbvrexcsf 3897 nfdif 4084 rabsnifsb 4690 nfpo 5577 nffr 5636 rexxpf 5835 boxcutc 8945 nfoi 9483 rabssnn0fi 14040 fsuppmapnn0fiubex 14046 sumodd 16468 nosupbnd1 27929 nosupbnd2 27931 noinfbnd1 27944 noinfbnd2 27946 fprodex01 33239 ordtconnlem1 34378 esumrnmpt2 34522 ddemeas 34691 bnj1388 35486 bnj1398 35487 bnj1445 35497 bnj1449 35501 regsfromsetind 37107 finxpreclem6 38099 wl-nfnae1 38240 cdlemefs32sn1aw 41246 ss2iundf 44443 ax6e2ndeqALT 45697 uzwo4 45831 eliin2f 45880 stoweidlem55 46827 stoweidlem59 46831 etransclem32 47038 salexct 47106 sge0f1o 47154 incsmflem 47513 decsmflem 47538 r19.32 47893 |
| Copyright terms: Public domain | W3C validator |