![]() |
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 1852. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1779 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 1852 | . 2 ⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ Ⅎ𝑥 ¬ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 Ⅎwnf 1778 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 |
This theorem depends on definitions: df-bi 206 df-or 846 df-ex 1775 df-nf 1779 |
This theorem is referenced by: nfnan 1896 nfor 1900 nfnaewOLD 2139 nfa1 2141 nfna1 2142 nfan1 2189 19.32 2222 nfex 2313 cbvexv1 2333 cbvex2v 2335 cbvex 2393 cbvex2 2406 nfnae 2428 axc14 2457 euor 2600 euor2 2602 nfne 3033 nfnel 3044 cbvrexfw 3293 cbvrexf 3345 ceqsex 3513 spcimegf 3575 spcegf 3577 spc2d 3587 cbvrexcsf 3937 nfdif 4121 nfdifOLD 4122 rabsnifsb 4721 0nelopabOLD 5564 nfpo 5589 nffr 5646 rexxpf 5844 boxcutc 8959 nfoi 9547 rabssnn0fi 13997 fsuppmapnn0fiubex 14003 sumodd 16382 nosupbnd1 27738 nosupbnd2 27740 noinfbnd1 27753 noinfbnd2 27755 fprodex01 32726 ordtconnlem1 33749 esumrnmpt2 33911 ddemeas 34079 bnj1388 34888 bnj1398 34889 bnj1445 34899 bnj1449 34903 finxpreclem6 37113 wl-nfnae1 37233 cdlemefs32sn1aw 40123 nfa1w 42365 ss2iundf 43360 ax6e2ndeqALT 44641 uzwo4 44688 eliin2f 44739 stoweidlem55 45709 stoweidlem59 45713 etransclem32 45920 salexct 45988 sge0f1o 46036 incsmflem 46395 decsmflem 46420 r19.32 46744 |
Copyright terms: Public domain | W3C validator |