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  2360  cbvexv1  2377  cbvex2v  2379  cbvex  2434  cbvex2  2447  nfnae  2469  axc14  2498  euor  2642  euor2  2644  nfne  3064  nfnel  3075  cbvrexfw  3309  cbvrexf  3353  ceqsex  3505  spcimegf  3522  spcegf  3554  spc2d  3564  cbvrexcsf  3899  nfdif  4087  rabsnifsb  4691  nfpo  5578  nffr  5637  rexxpf  5836  boxcutc  8941  nfoi  9478  rabssnn0fi  14033  fsuppmapnn0fiubex  14039  sumodd  16456  nosupbnd1  27893  nosupbnd2  27895  noinfbnd1  27908  noinfbnd2  27910  fprodex01  33184  ordtconnlem1  34327  esumrnmpt2  34471  ddemeas  34639  bnj1388  35434  bnj1398  35435  bnj1445  35445  bnj1449  35449  regsfromsetind  37082  finxpreclem6  38074  wl-nfnae1  38215  cdlemefs32sn1aw  41220  ss2iundf  44417  ax6e2ndeqALT  45671  uzwo4  45805  eliin2f  45854  stoweidlem55  46801  stoweidlem59  46805  etransclem32  47012  salexct  47080  sge0f1o  47128  incsmflem  47487  decsmflem  47512  r19.32  47867