Theorem nfn 1890

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

This proof depends on syntax axioms:  ¬ wn 3  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-or 862  df-ex 1813  df-nf 1817

This theorem is used by:  nfnan  1933  nfor  1937  nfa1  2188  nfna1  2189  nfan1  2237  19.32  2270  nfex  2355  cbvexv1  2372  cbvex2v  2374  cbvex  2429  cbvex2  2442  nfnae  2464  axc14  2493  euor  2637  euor2  2639  nfne  3059  nfnel  3070  cbvrexfw  3304  cbvrexf  3347  ceqsex  3498  spcimegf  3515  spcegf  3547  spc2d  3557  cbvrexcsf  3890  nfdif  4077  rabsnifsb  4683  nfpo  5565  nffr  5624  rexxpf  5825  boxcutc  8962  nfoi  9501  rabssnn0fi  14122  fsuppmapnn0fiubex  14128  sumodd  16551  nosupbnd1  28064  nosupbnd2  28066  noinfbnd1  28079  noinfbnd2  28081  fprodex01  33409  ordtconnlem1  34549  esumrnmpt2  34693  ddemeas  34862  bnj1388  35656  bnj1398  35657  bnj1445  35667  bnj1449  35671  regsfromsetind  37307  finxpreclem6  38299  wl-nfnae1  38440  cdlemefs32sn1aw  41451  ss2iundf  44644  ax6e2ndeqALT  45898  uzwo4  46039  eliin2f  46088  stoweidlem55  47034  stoweidlem59  47038  etransclem32  47245  salexct  47313  sge0f1o  47361  incsmflem  47720  decsmflem  47745  r19.32  48137