Theorem nfn 1857

Description: Inference associated with nfnt 1856. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1784 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 1783

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

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfnan  1900  nfor  1904  nfa1  2152  nfna1  2153  nfan1  2201  19.32  2234  nfex  2323  cbvexv1  2340  cbvex2v  2342  cbvex  2397  cbvex2  2410  nfnae  2432  axc14  2461  euor  2604  euor2  2606  nfne  3026  nfnel  3037  cbvrexfw  3270  cbvrexf  3324  ceqsex  3485  spcimegf  3506  spcegf  3547  spc2d  3557  cbvrexcsf  3894  nfdif  4080  nfdifOLD  4081  rabsnifsb  4674  nfpo  5533  nffr  5592  rexxpf  5790  boxcutc  8868  nfoi  9406  rabssnn0fi  13893  fsuppmapnn0fiubex  13899  sumodd  16299  nosupbnd1  27624  nosupbnd2  27626  noinfbnd1  27639  noinfbnd2  27641  fprodex01  32770  ordtconnlem1  33891  esumrnmpt2  34035  ddemeas  34203  bnj1388  35000  bnj1398  35001  bnj1445  35011  bnj1449  35015  finxpreclem6  37370  wl-nfnae1  37502  cdlemefs32sn1aw  40393  ss2iundf  43632  ax6e2ndeqALT  44904  uzwo4  45031  eliin2f  45082  stoweidlem55  46036  stoweidlem59  46040  etransclem32  46247  salexct  46315  sge0f1o  46363  incsmflem  46722  decsmflem  46747  r19.32  47082