Theorem nfn 1856

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

Syntax hints:  ¬ wn 3  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 209  df-or 844  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfnan  1900  nfor  1904  nfnaew  2152  nfa1  2154  nfna1  2155  nfan1  2199  19.32  2234  nfex  2342  cbvexv1  2361  cbvex2v  2364  cbvex  2416  cbvex2  2433  nfnae  2455  axc14  2485  euor  2694  euor2  2696  nfne  3122  nfnel  3133  cbvrexfw  3441  cbvrexf  3443  spcimegf  3592  spcegf  3594  spc2d  3606  cbvrexcsf  3929  nfdif  4105  rabsnifsb  4661  0nelopab  5455  nfpo  5482  nffr  5532  rexxpf  5721  boxcutc  8508  nfoi  8981  rabssnn0fi  13357  fsuppmapnn0fiubex  13363  sumodd  15742  fprodex01  30545  ordtconnlem1  31171  esumrnmpt2  31331  ddemeas  31499  bnj1388  32309  bnj1398  32310  bnj1445  32320  bnj1449  32324  nosupbnd1  33218  nosupbnd2  33220  finxpreclem6  34681  wl-nfnae1  34772  cdlemefs32sn1aw  37554  ss2iundf  40010  ax6e2ndeqALT  41271  uzwo4  41321  eliin2f  41376  stoweidlem55  42347  stoweidlem59  42351  etransclem32  42558  salexct  42624  sge0f1o  42671  incsmflem  43025  decsmflem  43049  r19.32  43303