Theorem nfn 1855

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

Syntax hints:  ¬ wn 3  Ⅎwnf 1780

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

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1777  df-nf 1781

This theorem is referenced by:  nfnan  1898  nfor  1902  nfa1  2149  nfna1  2150  nfan1  2198  19.32  2231  nfex  2323  cbvexv1  2343  cbvex2v  2345  cbvex  2402  cbvex2  2415  nfnae  2437  axc14  2466  euor  2609  euor2  2611  nfne  3041  nfnel  3052  cbvrexfw  3303  cbvrexf  3359  ceqsex  3528  spcimegf  3551  spcegf  3592  spc2d  3602  cbvrexcsf  3954  nfdif  4139  nfdifOLD  4140  rabsnifsb  4727  nfpo  5603  nffr  5662  rexxpf  5861  boxcutc  8980  nfoi  9552  rabssnn0fi  14024  fsuppmapnn0fiubex  14030  sumodd  16422  nosupbnd1  27774  nosupbnd2  27776  noinfbnd1  27789  noinfbnd2  27791  fprodex01  32832  ordtconnlem1  33885  esumrnmpt2  34049  ddemeas  34217  bnj1388  35026  bnj1398  35027  bnj1445  35037  bnj1449  35041  finxpreclem6  37379  wl-nfnae1  37509  cdlemefs32sn1aw  40397  ss2iundf  43649  ax6e2ndeqALT  44929  uzwo4  44993  eliin2f  45044  stoweidlem55  46011  stoweidlem59  46015  etransclem32  46222  salexct  46290  sge0f1o  46338  incsmflem  46697  decsmflem  46722  r19.32  47048