Theorem nfn 1877

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

Syntax hints:  ¬ wn 3  Ⅎwnf 1803

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

This theorem depends on definitions:  df-bi 209  df-or 859  df-ex 1800  df-nf 1804

This theorem is referenced by:  nfnan  1920  nfor  1924  nfa1  2185  nfna1  2186  nfan1  2235  19.32  2268  nfex  2356  cbvexv1  2373  cbvex2v  2375  cbvex  2430  cbvex2  2443  nfnae  2465  axc14  2494  euor  2638  euor2  2640  nfne  3058  nfnel  3069  cbvrexfw  3303  cbvrexf  3348  ceqsex  3501  spcimegf  3519  spcegf  3551  spc2d  3561  cbvrexcsf  3895  nfdif  4083  rabsnifsb  4681  nfpo  5561  nffr  5620  rexxpf  5819  boxcutc  8923  nfoi  9462  rabssnn0fi  13999  fsuppmapnn0fiubex  14005  sumodd  16422  nosupbnd1  27775  nosupbnd2  27777  noinfbnd1  27790  noinfbnd2  27792  fprodex01  33024  ordtconnlem1  34218  esumrnmpt2  34362  ddemeas  34530  bnj1388  35325  bnj1398  35326  bnj1445  35336  bnj1449  35340  regsfromsetind  36896  finxpreclem6  37887  wl-nfnae1  38028  cdlemefs32sn1aw  41035  ss2iundf  44232  ax6e2ndeqALT  45503  uzwo4  45630  eliin2f  45679  stoweidlem55  46626  stoweidlem59  46630  etransclem32  46837  salexct  46905  sge0f1o  46953  incsmflem  47312  decsmflem  47337  r19.32  47689