Theorem nfn 1824

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

Syntax hints:  ¬ wn 3  Ⅎwnf 1748

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

This theorem depends on definitions:  df-bi 197  df-or 384  df-ex 1745  df-nf 1750

This theorem is referenced by:  nfanOLD  1869  nfnan  1870  nfor  1874  nfa1  2068  nfna1  2069  nfan1  2106  19.32  2139  nfex  2192  cbvexv1  2212  cbvex  2308  cbvex2  2316  nfnae  2351  axc14  2400  euor  2541  euor2  2543  nfne  2923  nfnel  2933  cbvrexf  3196  spcimegf  3318  spcegf  3320  cbvrexcsf  3599  nfdif  3764  rabsnifsb  4289  nfpo  5069  nffr  5117  rexxpf  5302  0neqopab  6740  boxcutc  7993  nfoi  8460  rabssnn0fi  12825  fsuppmapnn0fiubex  12832  sumodd  15158  spc2d  29441  fprodex01  29699  ordtconnlem1  30098  esumrnmpt2  30258  ddemeas  30427  bnj1388  31227  bnj1398  31228  bnj1445  31238  bnj1449  31242  nosupbnd1  31985  nosupbnd2  31987  bj-cbvex2v  32863  finxpreclem6  33363  wl-nfnae1  33446  cdlemefs32sn1aw  36019  ss2iundf  38268  ax6e2ndeqALT  39481  uzwo4  39535  eliin2f  39601  stoweidlem55  40590  stoweidlem59  40594  etransclem32  40801  salexct  40870  sge0f1o  40917  incsmflem  41271  decsmflem  41295  r19.32  41488