Theorem nfn 1838

Description: Inference associated with nfnt 1837. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1766 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 1837	. 2 ⊢ (Ⅎ𝑥𝜑 → Ⅎ𝑥 ¬ 𝜑)
3	1, 2	ax-mp 5	1 ⊢ Ⅎ𝑥 ¬ 𝜑

Syntax hints:  ¬ wn 3  Ⅎwnf 1765

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

This theorem depends on definitions:  df-bi 208  df-or 843  df-ex 1762  df-nf 1766

This theorem is referenced by:  nfnan  1882  nfor  1886  nfa1  2121  nfna1  2122  nfan1  2165  19.32  2200  nfex  2306  cbvexv1  2321  cbvex  2373  cbvex2  2390  nfnae  2413  axc14  2443  euor  2662  euor2  2665  nfne  3087  nfnel  3097  cbvrexf  3398  spcimegf  3532  spcegf  3534  spc2d  3545  cbvrexcsf  3850  nfdif  4023  rabsnifsb  4565  0nelopab  5340  nfpo  5367  nffr  5417  rexxpf  5604  boxcutc  8353  nfoi  8824  rabssnn0fi  13204  fsuppmapnn0fiubex  13210  sumodd  15572  fprodex01  30225  ordtconnlem1  30784  esumrnmpt2  30944  ddemeas  31112  bnj1388  31919  bnj1398  31920  bnj1445  31930  bnj1449  31934  nosupbnd1  32823  nosupbnd2  32825  bj-cbvex2v  33669  finxpreclem6  34208  wl-nfnae1  34301  cdlemefs32sn1aw  37081  ss2iundf  39489  ax6e2ndeqALT  40804  uzwo4  40854  eliin2f  40910  stoweidlem55  41882  stoweidlem59  41886  etransclem32  42093  salexct  42159  sge0f1o  42206  incsmflem  42560  decsmflem  42584  r19.32  42812