Theorem nfn 1887

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

Syntax hints:  ¬ wn 3  Ⅎwnf 1813

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

This theorem depends on definitions:  df-bi 210  df-or 861  df-ex 1810  df-nf 1814

This theorem is referenced by:  nfnan  1930  nfor  1934  nfa1  2186  nfna1  2187  nfan1  2236  19.32  2269  nfex  2357  cbvexv1  2374  cbvex2v  2376  cbvex  2431  cbvex2  2444  nfnae  2466  axc14  2495  euor  2639  euor2  2641  nfne  3061  nfnel  3072  cbvrexfw  3306  cbvrexf  3350  ceqsex  3502  spcimegf  3519  spcegf  3551  spc2d  3561  cbvrexcsf  3896  nfdif  4084  rabsnifsb  4688  nfpo  5575  nffr  5634  rexxpf  5833  boxcutc  8935  nfoi  9472  rabssnn0fi  14018  fsuppmapnn0fiubex  14024  sumodd  16441  nosupbnd1  27878  nosupbnd2  27880  noinfbnd1  27893  noinfbnd2  27895  fprodex01  33169  ordtconnlem1  34314  esumrnmpt2  34458  ddemeas  34626  bnj1388  35421  bnj1398  35422  bnj1445  35432  bnj1449  35436  regsfromsetind  37050  finxpreclem6  38042  wl-nfnae1  38183  cdlemefs32sn1aw  41188  ss2iundf  44385  ax6e2ndeqALT  45639  uzwo4  45773  eliin2f  45822  stoweidlem55  46769  stoweidlem59  46773  etransclem32  46980  salexct  47048  sge0f1o  47096  incsmflem  47455  decsmflem  47480  r19.32  47835