Theorem nfn 1861

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

Syntax hints:  ¬ wn 3  Ⅎwnf 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812

This theorem depends on definitions:  df-bi 206  df-or 847  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfnan  1904  nfor  1908  nfnaewOLD  2147  nfa1  2149  nfna1  2150  nfan1  2194  19.32  2227  nfex  2318  cbvexv1  2339  cbvex2v  2341  cbvex  2399  cbvex2  2412  nfnae  2434  axc14  2463  euor  2608  euor2  2610  nfne  3044  nfnel  3055  cbvrexfw  3303  cbvrexf  3358  ceqsex  3524  spcimegf  3581  spcegf  3583  spc2d  3593  cbvrexcsf  3940  nfdif  4126  rabsnifsb  4727  0nelopabOLD  5569  nfpo  5594  nffr  5651  rexxpf  5848  boxcutc  8935  nfoi  9509  rabssnn0fi  13951  fsuppmapnn0fiubex  13957  sumodd  16331  nosupbnd1  27217  nosupbnd2  27219  noinfbnd1  27232  noinfbnd2  27234  fprodex01  32031  ordtconnlem1  32904  esumrnmpt2  33066  ddemeas  33234  bnj1388  34044  bnj1398  34045  bnj1445  34055  bnj1449  34059  finxpreclem6  36277  wl-nfnae1  36397  cdlemefs32sn1aw  39285  ss2iundf  42410  ax6e2ndeqALT  43692  uzwo4  43740  eliin2f  43793  stoweidlem55  44771  stoweidlem59  44775  etransclem32  44982  salexct  45050  sge0f1o  45098  incsmflem  45457  decsmflem  45482  r19.32  45806