Theorem nfn 1857

Description: Inference associated with nfnt 1856. (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 1856	. 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 207  df-or 848  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfnan  1900  nfor  1904  nfa1  2152  nfna1  2153  nfan1  2201  19.32  2234  nfex  2323  cbvexv1  2340  cbvex2v  2342  cbvex  2397  cbvex2  2410  nfnae  2432  axc14  2461  euor  2604  euor2  2606  nfne  3026  nfnel  3037  cbvrexfw  3277  cbvrexf  3332  ceqsex  3493  spcimegf  3514  spcegf  3555  spc2d  3565  cbvrexcsf  3902  nfdif  4088  nfdifOLD  4089  rabsnifsb  4682  nfpo  5545  nffr  5604  rexxpf  5801  boxcutc  8891  nfoi  9443  rabssnn0fi  13927  fsuppmapnn0fiubex  13933  sumodd  16334  nosupbnd1  27602  nosupbnd2  27604  noinfbnd1  27617  noinfbnd2  27619  fprodex01  32723  ordtconnlem1  33887  esumrnmpt2  34031  ddemeas  34199  bnj1388  34996  bnj1398  34997  bnj1445  35007  bnj1449  35011  finxpreclem6  37357  wl-nfnae1  37489  cdlemefs32sn1aw  40381  ss2iundf  43621  ax6e2ndeqALT  44893  uzwo4  45020  eliin2f  45071  stoweidlem55  46026  stoweidlem59  46030  etransclem32  46237  salexct  46305  sge0f1o  46353  incsmflem  46712  decsmflem  46737  r19.32  47072