|   | 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 1855. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1783 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 1855 | . 2 ⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ Ⅎ𝑥 ¬ 𝜑 | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 Ⅎwnf 1782 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 | 
| This theorem depends on definitions: df-bi 207 df-or 848 df-ex 1779 df-nf 1783 | 
| This theorem is referenced by: nfnan 1899 nfor 1903 nfa1 2150 nfna1 2151 nfan1 2199 19.32 2232 nfex 2323 cbvexv1 2343 cbvex2v 2345 cbvex 2403 cbvex2 2416 nfnae 2438 axc14 2467 euor 2610 euor2 2612 nfne 3042 nfnel 3053 cbvrexfw 3304 cbvrexf 3360 ceqsex 3529 spcimegf 3550 spcegf 3591 spc2d 3601 cbvrexcsf 3941 nfdif 4128 nfdifOLD 4129 rabsnifsb 4721 nfpo 5597 nffr 5657 rexxpf 5857 boxcutc 8982 nfoi 9555 rabssnn0fi 14028 fsuppmapnn0fiubex 14034 sumodd 16426 nosupbnd1 27760 nosupbnd2 27762 noinfbnd1 27775 noinfbnd2 27777 fprodex01 32828 ordtconnlem1 33924 esumrnmpt2 34070 ddemeas 34238 bnj1388 35048 bnj1398 35049 bnj1445 35059 bnj1449 35063 finxpreclem6 37398 wl-nfnae1 37530 cdlemefs32sn1aw 40417 ss2iundf 43677 ax6e2ndeqALT 44956 uzwo4 45063 eliin2f 45114 stoweidlem55 46075 stoweidlem59 46079 etransclem32 46286 salexct 46354 sge0f1o 46402 incsmflem 46761 decsmflem 46786 r19.32 47115 | 
| Copyright terms: Public domain | W3C validator |