Theorem nfn 1859

Description: Inference associated with nfnt 1858. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1786 changed. (Revised by Wolf Lammen, 18-Sep-2021.)

Hypothesis

Ref	Expression
nfn.1	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
nfn	⊢ Ⅎ𝑥 ¬ 𝜑

Proof of Theorem nfn

Step	Hyp	Ref	Expression
1		nfn.1	. 2 ⊢ Ⅎ𝑥𝜑
2		nfnt 1858	. 2 ⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑)
3	1, 2	ax-mp 5	1 ⊢ Ⅎ𝑥 ¬ 𝜑

Syntax hints:  ¬ wn 3  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811

This theorem depends on definitions:  df-bi 207  df-or 849  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfnan  1902  nfor  1906  nfa1  2157  nfna1  2158  nfan1  2208  19.32  2241  nfex  2330  cbvexv1  2347  cbvex2v  2349  cbvex  2404  cbvex2  2417  nfnae  2439  axc14  2468  euor  2612  euor2  2614  nfne  3034  nfnel  3045  cbvrexfw  3279  cbvrexf  3324  ceqsex  3478  spcimegf  3497  spcegf  3535  spc2d  3545  cbvrexcsf  3881  nfdif  4070  nfdifOLD  4071  rabsnifsb  4667  nfpo  5539  nffr  5598  rexxpf  5797  boxcutc  8883  nfoi  9423  rabssnn0fi  13942  fsuppmapnn0fiubex  13948  sumodd  16351  nosupbnd1  27695  nosupbnd2  27697  noinfbnd1  27710  noinfbnd2  27712  fprodex01  32916  ordtconnlem1  34087  esumrnmpt2  34231  ddemeas  34399  bnj1388  35194  bnj1398  35195  bnj1445  35205  bnj1449  35209  regsfromsetind  36740  finxpreclem6  37729  wl-nfnae1  37870  cdlemefs32sn1aw  40877  ss2iundf  44107  ax6e2ndeqALT  45378  uzwo4  45505  eliin2f  45555  stoweidlem55  46504  stoweidlem59  46508  etransclem32  46715  salexct  46783  sge0f1o  46831  incsmflem  47190  decsmflem  47215  r19.32  47561