Theorem nfn 1857

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

Syntax hints:  ¬ wn 3  Ⅎwnf 1784

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

This theorem depends on definitions:  df-bi 209  df-or 844  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfnan  1901  nfor  1905  nfnaew  2153  nfa1  2155  nfna1  2156  nfan1  2200  19.32  2235  nfex  2343  cbvexv1  2362  cbvex2v  2365  cbvex  2417  cbvex2  2434  nfnae  2456  axc14  2486  euor  2695  euor2  2697  nfne  3119  nfnel  3130  cbvrexfw  3438  cbvrexf  3440  spcimegf  3589  spcegf  3591  spc2d  3603  cbvrexcsf  3926  nfdif  4102  rabsnifsb  4658  0nelopab  5452  nfpo  5479  nffr  5529  rexxpf  5718  boxcutc  8505  nfoi  8978  rabssnn0fi  13355  fsuppmapnn0fiubex  13361  sumodd  15739  fprodex01  30541  ordtconnlem1  31167  esumrnmpt2  31327  ddemeas  31495  bnj1388  32305  bnj1398  32306  bnj1445  32316  bnj1449  32320  nosupbnd1  33214  nosupbnd2  33216  finxpreclem6  34680  wl-nfnae1  34783  cdlemefs32sn1aw  37565  ss2iundf  40024  ax6e2ndeqALT  41285  uzwo4  41335  eliin2f  41390  stoweidlem55  42360  stoweidlem59  42364  etransclem32  42571  salexct  42637  sge0f1o  42684  incsmflem  43038  decsmflem  43062  r19.32  43316