| 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 1857. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1785 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 1857 | . 2 ⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ Ⅎ𝑥 ¬ 𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 Ⅎwnf 1784 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 |
| This theorem depends on definitions: df-bi 207 df-or 848 df-ex 1781 df-nf 1785 |
| This theorem is referenced by: nfnan 1901 nfor 1905 nfa1 2156 nfna1 2157 nfan1 2207 19.32 2240 nfex 2329 cbvexv1 2346 cbvex2v 2348 cbvex 2403 cbvex2 2416 nfnae 2438 axc14 2467 euor 2611 euor2 2613 nfne 3033 nfnel 3044 cbvrexfw 3277 cbvrexf 3331 ceqsex 3489 spcimegf 3508 spcegf 3546 spc2d 3556 cbvrexcsf 3892 nfdif 4081 nfdifOLD 4082 rabsnifsb 4679 nfpo 5538 nffr 5597 rexxpf 5796 boxcutc 8879 nfoi 9419 rabssnn0fi 13909 fsuppmapnn0fiubex 13915 sumodd 16315 nosupbnd1 27682 nosupbnd2 27684 noinfbnd1 27697 noinfbnd2 27699 fprodex01 32906 ordtconnlem1 34081 esumrnmpt2 34225 ddemeas 34393 bnj1388 35189 bnj1398 35190 bnj1445 35200 bnj1449 35204 regsfromsetind 36669 finxpreclem6 37601 wl-nfnae1 37733 cdlemefs32sn1aw 40674 ss2iundf 43900 ax6e2ndeqALT 45171 uzwo4 45298 eliin2f 45348 stoweidlem55 46299 stoweidlem59 46303 etransclem32 46510 salexct 46578 sge0f1o 46626 incsmflem 46985 decsmflem 47010 r19.32 47344 |
| Copyright terms: Public domain | W3C validator |