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  2207  19.32  2240  nfex  2329  cbvexv1  2346  cbvex2v  2348  cbvex  2403  cbvex2  2416  nfnae  2438  axc14  2467  euor  2611  euor2  2613  nfne  3033  nfnel  3044  cbvrexfw  3277  cbvrexf  3331  ceqsex  3489  spcimegf  3508  spcegf  3546  spc2d  3556  cbvrexcsf  3892  nfdif  4081  nfdifOLD  4082  rabsnifsb  4679  nfpo  5538  nffr  5597  rexxpf  5796  boxcutc  8879  nfoi  9419  rabssnn0fi  13909  fsuppmapnn0fiubex  13915  sumodd  16315  nosupbnd1  27682  nosupbnd2  27684  noinfbnd1  27697  noinfbnd2  27699  fprodex01  32906  ordtconnlem1  34081  esumrnmpt2  34225  ddemeas  34393  bnj1388  35189  bnj1398  35190  bnj1445  35200  bnj1449  35204  regsfromsetind  36669  finxpreclem6  37601  wl-nfnae1  37733  cdlemefs32sn1aw  40674  ss2iundf  43900  ax6e2ndeqALT  45171  uzwo4  45298  eliin2f  45348  stoweidlem55  46299  stoweidlem59  46303  etransclem32  46510  salexct  46578  sge0f1o  46626  incsmflem  46985  decsmflem  47010  r19.32  47344