Theorem nfn 1865

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

Syntax hints:  ¬ wn 3  Ⅎwnf 1791

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

This theorem depends on definitions:  df-bi 210  df-or 848  df-ex 1788  df-nf 1792

This theorem is referenced by:  nfnan  1908  nfor  1912  nfnaewOLD  2152  nfa1  2154  nfna1  2155  nfan1  2200  19.32  2233  nfex  2325  cbvexv1  2343  cbvex2v  2346  cbvex  2398  cbvex2  2411  nfnae  2433  axc14  2462  euor  2612  euor2  2614  nfne  3032  nfnel  3043  cbvrexfw  3336  cbvrexf  3338  spcimegf  3495  spcegf  3497  spc2d  3507  cbvrexcsf  3844  nfdif  4026  rabsnifsb  4624  0nelopabOLD  5432  nfpo  5458  nffr  5510  rexxpf  5701  boxcutc  8600  nfoi  9108  rabssnn0fi  13524  fsuppmapnn0fiubex  13530  sumodd  15912  fprodex01  30813  ordtconnlem1  31542  esumrnmpt2  31702  ddemeas  31870  bnj1388  32680  bnj1398  32681  bnj1445  32691  bnj1449  32695  nosupbnd1  33603  nosupbnd2  33605  noinfbnd1  33618  noinfbnd2  33620  finxpreclem6  35253  wl-nfnae1  35373  cdlemefs32sn1aw  38114  ss2iundf  40885  ax6e2ndeqALT  42165  uzwo4  42215  eliin2f  42268  stoweidlem55  43214  stoweidlem59  43218  etransclem32  43425  salexct  43491  sge0f1o  43538  incsmflem  43892  decsmflem  43916  r19.32  44205