Theorem nfn 1860

Description: Inference associated with nfnt 1859. (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 1859	. 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 206  df-or 846  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfnan  1903  nfor  1907  nfnaewOLD  2146  nfa1  2148  nfna1  2149  nfan1  2193  19.32  2226  nfex  2317  cbvexv1  2338  cbvex2v  2340  cbvex  2398  cbvex2  2411  nfnae  2433  axc14  2462  euor  2607  euor2  2609  nfne  3043  nfnel  3054  cbvrexfw  3302  cbvrexf  3357  ceqsex  3523  spcimegf  3580  spcegf  3582  spc2d  3592  cbvrexcsf  3939  nfdif  4125  rabsnifsb  4726  0nelopabOLD  5568  nfpo  5593  nffr  5650  rexxpf  5847  boxcutc  8934  nfoi  9508  rabssnn0fi  13950  fsuppmapnn0fiubex  13956  sumodd  16330  nosupbnd1  27214  nosupbnd2  27216  noinfbnd1  27229  noinfbnd2  27231  fprodex01  32026  ordtconnlem1  32899  esumrnmpt2  33061  ddemeas  33229  bnj1388  34039  bnj1398  34040  bnj1445  34050  bnj1449  34054  finxpreclem6  36272  wl-nfnae1  36392  cdlemefs32sn1aw  39280  ss2iundf  42400  ax6e2ndeqALT  43682  uzwo4  43730  eliin2f  43783  stoweidlem55  44761  stoweidlem59  44765  etransclem32  44972  salexct  45040  sge0f1o  45088  incsmflem  45447  decsmflem  45472  r19.32  45796