Theorem nfn 1861

Description: Inference associated with nfnt 1860. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1788 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 1787

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

This theorem depends on definitions:  df-bi 206  df-or 844  df-ex 1784  df-nf 1788

This theorem is referenced by:  nfnan  1904  nfor  1908  nfnaewOLD  2148  nfa1  2150  nfna1  2151  nfan1  2196  19.32  2229  nfex  2322  cbvexv1  2341  cbvex2v  2344  cbvex  2399  cbvex2  2412  nfnae  2434  axc14  2463  euor  2613  euor2  2615  nfne  3044  nfnel  3055  cbvrexfw  3360  cbvrexf  3362  spcimegf  3519  spcegf  3521  spc2d  3531  cbvrexcsf  3874  nfdif  4056  rabsnifsb  4655  0nelopabOLD  5472  nfpo  5499  nffr  5554  rexxpf  5745  boxcutc  8687  nfoi  9203  rabssnn0fi  13634  fsuppmapnn0fiubex  13640  sumodd  16025  fprodex01  31041  ordtconnlem1  31776  esumrnmpt2  31936  ddemeas  32104  bnj1388  32913  bnj1398  32914  bnj1445  32924  bnj1449  32928  nosupbnd1  33844  nosupbnd2  33846  noinfbnd1  33859  noinfbnd2  33861  finxpreclem6  35494  wl-nfnae1  35614  cdlemefs32sn1aw  38355  ss2iundf  41156  ax6e2ndeqALT  42440  uzwo4  42490  eliin2f  42543  stoweidlem55  43486  stoweidlem59  43490  etransclem32  43697  salexct  43763  sge0f1o  43810  incsmflem  44164  decsmflem  44188  r19.32  44477