Theorem nfn 1859

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

Syntax hints:  ¬ wn 3  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 207  df-or 849  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfnan  1902  nfor  1906  nfa1  2157  nfna1  2158  nfan1  2208  19.32  2241  nfex  2329  cbvexv1  2346  cbvex2v  2348  cbvex  2403  cbvex2  2416  nfnae  2438  axc14  2467  euor  2611  euor2  2613  nfne  3033  nfnel  3044  cbvrexfw  3278  cbvrexf  3323  ceqsex  3477  spcimegf  3496  spcegf  3534  spc2d  3544  cbvrexcsf  3880  nfdif  4069  nfdifOLD  4070  rabsnifsb  4666  nfpo  5545  nffr  5604  rexxpf  5802  boxcutc  8889  nfoi  9429  rabssnn0fi  13948  fsuppmapnn0fiubex  13954  sumodd  16357  nosupbnd1  27678  nosupbnd2  27680  noinfbnd1  27693  noinfbnd2  27695  fprodex01  32898  ordtconnlem1  34068  esumrnmpt2  34212  ddemeas  34380  bnj1388  35175  bnj1398  35176  bnj1445  35186  bnj1449  35190  regsfromsetind  36721  finxpreclem6  37712  wl-nfnae1  37853  cdlemefs32sn1aw  40860  ss2iundf  44086  ax6e2ndeqALT  45357  uzwo4  45484  eliin2f  45534  stoweidlem55  46483  stoweidlem59  46487  etransclem32  46694  salexct  46762  sge0f1o  46810  incsmflem  47169  decsmflem  47194  r19.32  47546