Theorem nfn 1954

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

Syntax hints:  ¬ wn 3  Ⅎwnf 1879

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

This theorem depends on definitions:  df-bi 199  df-or 875  df-ex 1876  df-nf 1880

This theorem is referenced by:  nfnan  2000  nfor  2004  nfa1  2195  nfna1  2196  nfan1  2232  nfan1OLDOLD  2233  19.32  2268  nfex  2330  cbvexv1  2341  cbvex  2388  cbvex2  2394  nfnae  2418  axc14  2468  sb8vv  2537  euor  2662  euor2  2665  nfne  3069  nfnel  3079  cbvrexf  3347  spcimegf  3473  spcegf  3475  cbvrexcsf  3759  nfdif  3927  rabsnifsb  4444  nfpo  5236  nffr  5284  rexxpf  5471  0neqopab  6930  boxcutc  8189  nfoi  8659  rabssnn0fi  13036  fsuppmapnn0fiubex  13042  sumodd  15444  spc2d  29830  fprodex01  30081  ordtconnlem1  30478  esumrnmpt2  30638  ddemeas  30807  bnj1388  31610  bnj1398  31611  bnj1445  31621  bnj1449  31625  nosupbnd1  32365  nosupbnd2  32367  bj-cbvex2v  33234  finxpreclem6  33723  wl-nfnae1  33798  cdlemefs32sn1aw  36427  ss2iundf  38722  ax6e2ndeqALT  39915  uzwo4  39968  eliin2f  40033  stoweidlem55  41003  stoweidlem59  41007  etransclem32  41214  salexct  41283  sge0f1o  41330  incsmflem  41684  decsmflem  41708  r19.32  41933