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  2608  euor2  2610  nfne  3030  nfnel  3041  cbvrexfw  3274  cbvrexf  3328  ceqsex  3486  spcimegf  3505  spcegf  3543  spc2d  3553  cbvrexcsf  3889  nfdif  4078  nfdifOLD  4079  rabsnifsb  4674  nfpo  5533  nffr  5592  rexxpf  5791  boxcutc  8871  nfoi  9407  rabssnn0fi  13895  fsuppmapnn0fiubex  13901  sumodd  16301  nosupbnd1  27654  nosupbnd2  27656  noinfbnd1  27669  noinfbnd2  27671  fprodex01  32813  ordtconnlem1  33958  esumrnmpt2  34102  ddemeas  34270  bnj1388  35066  bnj1398  35067  bnj1445  35077  bnj1449  35081  finxpreclem6  37461  wl-nfnae1  37593  cdlemefs32sn1aw  40533  ss2iundf  43776  ax6e2ndeqALT  45047  uzwo4  45174  eliin2f  45225  stoweidlem55  46177  stoweidlem59  46181  etransclem32  46388  salexct  46456  sge0f1o  46504  incsmflem  46863  decsmflem  46888  r19.32  47222