![]() |
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 1931. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1859 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 1931 | . 2 ⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ Ⅎ𝑥 ¬ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 Ⅎwnf 1857 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 |
This theorem depends on definitions: df-bi 197 df-or 384 df-ex 1854 df-nf 1859 |
This theorem is referenced by: nfanOLD 1978 nfnan 1979 nfor 1983 nfa1 2177 nfna1 2178 nfan1 2215 19.32 2248 nfex 2301 cbvexv1 2321 cbvex 2417 cbvex2 2425 nfnae 2460 axc14 2509 euor 2650 euor2 2652 nfne 3032 nfnel 3042 cbvrexf 3305 spcimegf 3427 spcegf 3429 cbvrexcsf 3707 nfdif 3874 rabsnifsb 4401 nfpo 5192 nffr 5240 rexxpf 5425 0neqopab 6863 boxcutc 8117 nfoi 8584 rabssnn0fi 12979 fsuppmapnn0fiubex 12986 sumodd 15313 spc2d 29622 fprodex01 29880 ordtconnlem1 30279 esumrnmpt2 30439 ddemeas 30608 bnj1388 31408 bnj1398 31409 bnj1445 31419 bnj1449 31423 nosupbnd1 32166 nosupbnd2 32168 bj-cbvex2v 33044 finxpreclem6 33544 wl-nfnae1 33629 cdlemefs32sn1aw 36204 ss2iundf 38453 ax6e2ndeqALT 39666 uzwo4 39720 eliin2f 39786 stoweidlem55 40775 stoweidlem59 40779 etransclem32 40986 salexct 41055 sge0f1o 41102 incsmflem 41456 decsmflem 41480 r19.32 41673 |
Copyright terms: Public domain | W3C validator |