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  2154  nfna1  2155  nfan1  2203  19.32  2236  nfex  2325  cbvexv1  2342  cbvex2v  2344  cbvex  2399  cbvex2  2412  nfnae  2434  axc14  2463  euor  2606  euor2  2608  nfne  3029  nfnel  3040  cbvrexfw  3273  cbvrexf  3327  ceqsex  3485  spcimegf  3504  spcegf  3542  spc2d  3552  cbvrexcsf  3888  nfdif  4076  nfdifOLD  4077  rabsnifsb  4672  nfpo  5528  nffr  5587  rexxpf  5786  boxcutc  8865  nfoi  9400  rabssnn0fi  13893  fsuppmapnn0fiubex  13899  sumodd  16299  nosupbnd1  27653  nosupbnd2  27655  noinfbnd1  27668  noinfbnd2  27670  fprodex01  32808  ordtconnlem1  33937  esumrnmpt2  34081  ddemeas  34249  bnj1388  35045  bnj1398  35046  bnj1445  35056  bnj1449  35060  finxpreclem6  37438  wl-nfnae1  37570  cdlemefs32sn1aw  40461  ss2iundf  43700  ax6e2ndeqALT  44971  uzwo4  45098  eliin2f  45149  stoweidlem55  46101  stoweidlem59  46105  etransclem32  46312  salexct  46380  sge0f1o  46428  incsmflem  46787  decsmflem  46812  r19.32  47137