Theorem nfn 1864

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

Syntax hints:  ¬ wn 3  Ⅎwnf 1790

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

This theorem depends on definitions:  df-bi 206  df-or 845  df-ex 1787  df-nf 1791

This theorem is referenced by:  nfnan  1907  nfor  1911  nfnaewOLD  2150  nfa1  2152  nfna1  2153  nfan1  2197  19.32  2230  nfex  2322  cbvexv1  2343  cbvex2v  2346  cbvex  2401  cbvex2  2414  nfnae  2436  axc14  2465  euor  2615  euor2  2617  nfne  3047  nfnel  3058  cbvrexfw  3369  cbvrexf  3371  spcimegf  3528  spcegf  3530  spc2d  3540  cbvrexcsf  3883  nfdif  4065  rabsnifsb  4664  0nelopabOLD  5482  nfpo  5509  nffr  5564  rexxpf  5755  boxcutc  8712  nfoi  9251  rabssnn0fi  13704  fsuppmapnn0fiubex  13710  sumodd  16095  fprodex01  31135  ordtconnlem1  31870  esumrnmpt2  32032  ddemeas  32200  bnj1388  33009  bnj1398  33010  bnj1445  33020  bnj1449  33024  nosupbnd1  33913  nosupbnd2  33915  noinfbnd1  33928  noinfbnd2  33930  finxpreclem6  35563  wl-nfnae1  35683  cdlemefs32sn1aw  38424  ss2iundf  41237  ax6e2ndeqALT  42521  uzwo4  42571  eliin2f  42624  stoweidlem55  43567  stoweidlem59  43571  etransclem32  43778  salexct  43844  sge0f1o  43891  incsmflem  44245  decsmflem  44269  r19.32  44558