Theorem nfn 1889

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

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

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

This proof depends on definitions:  df-bi 210  df-or 862  df-ex 1812  df-nf 1816

This theorem is used by:  nfnan  1932  nfor  1936  nfa1  2187  nfna1  2188  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  4065  rabsnifsb  4679  nfpo  5565  nffr  5624  rexxpf  5826  boxcutc  8976  nfoi  9515  rabssnn0fi  14136  fsuppmapnn0fiubex  14142  sumodd  16567  nosupbnd1  28080  nosupbnd2  28082  noinfbnd1  28095  noinfbnd2  28097  fprodex01  33466  ordtconnlem1  34606  esumrnmpt2  34750  ddemeas  34919  bnj1388  35713  bnj1398  35714  bnj1445  35724  bnj1449  35728  rmo6  35760  regsfromsetind  37423  finxpreclem6  38428  wl-nfnae1  38569  cdlemefs32sn1aw  41580  ss2iundf  44768  ax6e2ndeqALT  46021  uzwo4  46178  eliin2f  46227  stoweidlem55  47173  stoweidlem59  47177  etransclem32  47384  salexct  47452  sge0f1o  47500  incsmflem  47859  decsmflem  47884  r19.32  48277