Theorem nfn 1864

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

Syntax hints:  ¬ wn 3  Ⅎwnf 1790

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

This theorem depends on definitions:  df-bi 208  df-or 854  df-ex 1787  df-nf 1791

This theorem is referenced by:  nfnan  1907  nfor  1911  nfa1  2162  nfna1  2163  nfan1  2212  19.32  2245  nfex  2333  cbvexv1  2350  cbvex2v  2352  cbvex  2407  cbvex2  2420  nfnae  2442  axc14  2471  euor  2615  euor2  2617  nfne  3035  nfnel  3046  cbvrexfw  3280  cbvrexf  3325  ceqsex  3478  spcimegf  3497  spcegf  3530  spc2d  3540  cbvrexcsf  3874  nfdif  4060  rabsnifsb  4654  nfpo  5532  nffr  5591  rexxpf  5789  boxcutc  8879  nfoi  9419  rabssnn0fi  13939  fsuppmapnn0fiubex  13945  sumodd  16348  nosupbnd1  27696  nosupbnd2  27698  noinfbnd1  27711  noinfbnd2  27713  fprodex01  32917  ordtconnlem1  34108  esumrnmpt2  34252  ddemeas  34420  bnj1388  35215  bnj1398  35216  bnj1445  35226  bnj1449  35230  regsfromsetind  36767  finxpreclem6  37758  wl-nfnae1  37899  cdlemefs32sn1aw  40906  ss2iundf  44103  ax6e2ndeqALT  45374  uzwo4  45501  eliin2f  45551  stoweidlem55  46498  stoweidlem59  46502  etransclem32  46709  salexct  46777  sge0f1o  46825  incsmflem  47184  decsmflem  47209  r19.32  47561