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  3279  cbvrexf  3335  ceqsex  3496  spcimegf  3517  spcegf  3558  spc2d  3568  cbvrexcsf  3905  nfdif  4092  nfdifOLD  4093  rabsnifsb  4686  nfpo  5552  nffr  5611  rexxpf  5811  boxcutc  8914  nfoi  9467  rabssnn0fi  13951  fsuppmapnn0fiubex  13957  sumodd  16358  nosupbnd1  27626  nosupbnd2  27628  noinfbnd1  27641  noinfbnd2  27643  fprodex01  32750  ordtconnlem1  33914  esumrnmpt2  34058  ddemeas  34226  bnj1388  35023  bnj1398  35024  bnj1445  35034  bnj1449  35038  finxpreclem6  37384  wl-nfnae1  37516  cdlemefs32sn1aw  40408  ss2iundf  43648  ax6e2ndeqALT  44920  uzwo4  45047  eliin2f  45098  stoweidlem55  46053  stoweidlem59  46057  etransclem32  46264  salexct  46332  sge0f1o  46380  incsmflem  46739  decsmflem  46764  r19.32  47096