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  2236  19.32  2269  nfex  2354  cbvexv1  2371  cbvex2v  2373  cbvex  2428  cbvex2  2441  nfnae  2463  axc14  2492  euor  2636  euor2  2638  nfne  3058  nfnel  3069  cbvrexfw  3303  cbvrexf  3346  ceqsex  3497  spcimegf  3514  spcegf  3546  spc2d  3556  cbvrexcsf  3890  nfdif  4077  rabsnifsb  4683  nfpo  5569  nffr  5628  rexxpf  5827  boxcutc  8948  nfoi  9486  rabssnn0fi  14050  fsuppmapnn0fiubex  14056  sumodd  16478  nosupbnd1  27950  nosupbnd2  27952  noinfbnd1  27965  noinfbnd2  27967  fprodex01  33295  ordtconnlem1  34434  esumrnmpt2  34578  ddemeas  34747  bnj1388  35542  bnj1398  35543  bnj1445  35553  bnj1449  35557  regsfromsetind  37158  finxpreclem6  38150  wl-nfnae1  38291  cdlemefs32sn1aw  41287  ss2iundf  44499  ax6e2ndeqALT  45753  uzwo4  45887  eliin2f  45936  stoweidlem55  46883  stoweidlem59  46887  etransclem32  47094  salexct  47162  sge0f1o  47210  incsmflem  47569  decsmflem  47594  r19.32  47986