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  2189  nfna1  2190  nfan1  2239  19.32  2272  nfex  2359  cbvexv1  2376  cbvex2v  2378  cbvex  2433  cbvex2  2446  nfnae  2468  axc14  2497  euor  2641  euor2  2643  nfne  3063  nfnel  3074  cbvrexfw  3308  cbvrexf  3352  ceqsex  3504  spcimegf  3521  spcegf  3553  spc2d  3563  cbvrexcsf  3897  nfdif  4084  rabsnifsb  4690  nfpo  5577  nffr  5636  rexxpf  5835  boxcutc  8945  nfoi  9483  rabssnn0fi  14040  fsuppmapnn0fiubex  14046  sumodd  16468  nosupbnd1  27929  nosupbnd2  27931  noinfbnd1  27944  noinfbnd2  27946  fprodex01  33239  ordtconnlem1  34378  esumrnmpt2  34522  ddemeas  34691  bnj1388  35486  bnj1398  35487  bnj1445  35497  bnj1449  35501  regsfromsetind  37107  finxpreclem6  38099  wl-nfnae1  38240  cdlemefs32sn1aw  41246  ss2iundf  44443  ax6e2ndeqALT  45697  uzwo4  45831  eliin2f  45880  stoweidlem55  46827  stoweidlem59  46831  etransclem32  47038  salexct  47106  sge0f1o  47154  incsmflem  47513  decsmflem  47538  r19.32  47893