Theorem nfn 1860

Description: Inference associated with nfnt 1859. (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 1859	. 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 845  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfnan  1903  nfor  1907  nfnaewOLD  2146  nfa1  2148  nfna1  2149  nfan1  2193  19.32  2226  nfex  2318  cbvexv1  2339  cbvex2v  2342  cbvex  2399  cbvex2  2412  nfnae  2434  axc14  2463  euor  2613  euor2  2615  nfne  3045  nfnel  3056  cbvrexfw  3370  cbvrexf  3372  spcimegf  3529  spcegf  3531  spc2d  3541  cbvrexcsf  3878  nfdif  4060  rabsnifsb  4658  0nelopabOLD  5481  nfpo  5508  nffr  5563  rexxpf  5756  boxcutc  8729  nfoi  9273  rabssnn0fi  13706  fsuppmapnn0fiubex  13712  sumodd  16097  fprodex01  31139  ordtconnlem1  31874  esumrnmpt2  32036  ddemeas  32204  bnj1388  33013  bnj1398  33014  bnj1445  33024  bnj1449  33028  nosupbnd1  33917  nosupbnd2  33919  noinfbnd1  33932  noinfbnd2  33934  finxpreclem6  35567  wl-nfnae1  35687  cdlemefs32sn1aw  38428  ss2iundf  41267  ax6e2ndeqALT  42551  uzwo4  42601  eliin2f  42654  stoweidlem55  43596  stoweidlem59  43600  etransclem32  43807  salexct  43873  sge0f1o  43920  incsmflem  44277  decsmflem  44301  r19.32  44590