Theorem nfn 1858

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

Syntax hints:  ¬ wn 3  Ⅎwnf 1784

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

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfnan  1901  nfor  1905  nfa1  2156  nfna1  2157  nfan1  2205  19.32  2238  nfex  2327  cbvexv1  2344  cbvex2v  2346  cbvex  2401  cbvex2  2414  nfnae  2436  axc14  2465  euor  2609  euor2  2611  nfne  3031  nfnel  3042  cbvrexfw  3275  cbvrexf  3329  ceqsex  3487  spcimegf  3506  spcegf  3544  spc2d  3554  cbvrexcsf  3890  nfdif  4079  nfdifOLD  4080  rabsnifsb  4677  nfpo  5536  nffr  5595  rexxpf  5794  boxcutc  8877  nfoi  9417  rabssnn0fi  13907  fsuppmapnn0fiubex  13913  sumodd  16313  nosupbnd1  27680  nosupbnd2  27682  noinfbnd1  27695  noinfbnd2  27697  fprodex01  32855  ordtconnlem1  34030  esumrnmpt2  34174  ddemeas  34342  bnj1388  35138  bnj1398  35139  bnj1445  35149  bnj1449  35153  finxpreclem6  37540  wl-nfnae1  37672  cdlemefs32sn1aw  40613  ss2iundf  43842  ax6e2ndeqALT  45113  uzwo4  45240  eliin2f  45290  stoweidlem55  46241  stoweidlem59  46245  etransclem32  46452  salexct  46520  sge0f1o  46568  incsmflem  46927  decsmflem  46952  r19.32  47286