Theorem nfn 1784

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

Syntax hints:  ¬ wn 3  Ⅎwnf 1708

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

This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1705  df-nf 1710

This theorem is referenced by:  nfanOLD  1829  nfnan  1830  nfor  1834  nfa1  2028  nfna1  2029  nfan1  2068  19.32  2101  nfex  2154  cbvexv1  2176  cbvex  2272  cbvex2  2280  nfnae  2318  axc14  2372  euor  2512  euor2  2514  nfne  2894  nfnel  2904  cbvrexf  3166  spcimegf  3287  spcegf  3289  cbvrexcsf  3566  nfdif  3731  rabsnifsb  4257  nfpo  5040  nffr  5088  rexxpf  5269  0neqopab  6698  boxcutc  7951  nfoi  8419  rabssnn0fi  12785  fsuppmapnn0fiubex  12792  sumodd  15111  spc2d  29313  fprodex01  29571  ordtconnlem1  29970  esumrnmpt2  30130  ddemeas  30299  bnj1388  31101  bnj1398  31102  bnj1445  31112  bnj1449  31116  nosupbnd1  31860  nosupbnd2  31862  bj-cbvex2v  32738  finxpreclem6  33233  wl-nfnae1  33316  cdlemefs32sn1aw  35702  ss2iundf  37951  ax6e2ndeqALT  39167  uzwo4  39221  eliin2f  39287  stoweidlem55  40272  stoweidlem59  40276  etransclem32  40483  salexct  40552  sge0f1o  40599  incsmflem  40950  decsmflem  40974  r19.32  41167