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  3277  cbvrexf  3332  ceqsex  3493  spcimegf  3514  spcegf  3555  spc2d  3565  cbvrexcsf  3902  nfdif  4088  nfdifOLD  4089  rabsnifsb  4682  nfpo  5545  nffr  5604  rexxpf  5801  boxcutc  8891  nfoi  9443  rabssnn0fi  13927  fsuppmapnn0fiubex  13933  sumodd  16334  nosupbnd1  27659  nosupbnd2  27661  noinfbnd1  27674  noinfbnd2  27676  fprodex01  32800  ordtconnlem1  33907  esumrnmpt2  34051  ddemeas  34219  bnj1388  35016  bnj1398  35017  bnj1445  35027  bnj1449  35031  finxpreclem6  37377  wl-nfnae1  37509  cdlemefs32sn1aw  40401  ss2iundf  43641  ax6e2ndeqALT  44913  uzwo4  45040  eliin2f  45091  stoweidlem55  46046  stoweidlem59  46050  etransclem32  46257  salexct  46325  sge0f1o  46373  incsmflem  46732  decsmflem  46757  r19.32  47092