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  2330  cbvexv1  2347  cbvex2v  2349  cbvex  2404  cbvex2  2417  nfnae  2439  axc14  2468  euor  2612  euor2  2614  nfne  3034  nfnel  3045  cbvrexfw  3279  cbvrexf  3333  ceqsex  3491  spcimegf  3510  spcegf  3548  spc2d  3558  cbvrexcsf  3894  nfdif  4083  nfdifOLD  4084  rabsnifsb  4681  nfpo  5546  nffr  5605  rexxpf  5804  boxcutc  8891  nfoi  9431  rabssnn0fi  13921  fsuppmapnn0fiubex  13927  sumodd  16327  nosupbnd1  27694  nosupbnd2  27696  noinfbnd1  27709  noinfbnd2  27711  fprodex01  32917  ordtconnlem1  34102  esumrnmpt2  34246  ddemeas  34414  bnj1388  35209  bnj1398  35210  bnj1445  35220  bnj1449  35224  regsfromsetind  36691  finxpreclem6  37651  wl-nfnae1  37783  cdlemefs32sn1aw  40790  ss2iundf  44015  ax6e2ndeqALT  45286  uzwo4  45413  eliin2f  45463  stoweidlem55  46413  stoweidlem59  46417  etransclem32  46624  salexct  46692  sge0f1o  46740  incsmflem  47099  decsmflem  47124  r19.32  47458