Theorem nfn 1853

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

Syntax hints:  ¬ wn 3  Ⅎwnf 1778

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

This theorem depends on definitions:  df-bi 206  df-or 846  df-ex 1775  df-nf 1779

This theorem is referenced by:  nfnan  1896  nfor  1900  nfnaewOLD  2139  nfa1  2141  nfna1  2142  nfan1  2189  19.32  2222  nfex  2313  cbvexv1  2333  cbvex2v  2335  cbvex  2393  cbvex2  2406  nfnae  2428  axc14  2457  euor  2600  euor2  2602  nfne  3033  nfnel  3044  cbvrexfw  3293  cbvrexf  3345  ceqsex  3513  spcimegf  3575  spcegf  3577  spc2d  3587  cbvrexcsf  3937  nfdif  4121  nfdifOLD  4122  rabsnifsb  4721  0nelopabOLD  5564  nfpo  5589  nffr  5646  rexxpf  5844  boxcutc  8959  nfoi  9547  rabssnn0fi  13997  fsuppmapnn0fiubex  14003  sumodd  16382  nosupbnd1  27738  nosupbnd2  27740  noinfbnd1  27753  noinfbnd2  27755  fprodex01  32726  ordtconnlem1  33749  esumrnmpt2  33911  ddemeas  34079  bnj1388  34888  bnj1398  34889  bnj1445  34899  bnj1449  34903  finxpreclem6  37113  wl-nfnae1  37233  cdlemefs32sn1aw  40123  nfa1w  42365  ss2iundf  43360  ax6e2ndeqALT  44641  uzwo4  44688  eliin2f  44739  stoweidlem55  45709  stoweidlem59  45713  etransclem32  45920  salexct  45988  sge0f1o  46036  incsmflem  46395  decsmflem  46420  r19.32  46744