Theorem nfn 1884

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

Syntax hints:  ¬ wn 3  Ⅎwnf 1810

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

This theorem depends on definitions:  df-bi 210  df-or 861  df-ex 1807  df-nf 1811

This theorem is referenced by:  nfnan  1927  nfor  1931  nfa1  2192  nfna1  2193  nfan1  2242  19.32  2275  nfex  2363  cbvexv1  2380  cbvex2v  2382  cbvex  2437  cbvex2  2450  nfnae  2472  axc14  2501  euor  2645  euor2  2647  nfne  3067  nfnel  3078  cbvrexfw  3312  cbvrexf  3357  ceqsex  3510  spcimegf  3528  spcegf  3560  spc2d  3570  cbvrexcsf  3904  nfdif  4092  rabsnifsb  4693  nfpo  5576  nffr  5635  rexxpf  5834  boxcutc  8938  nfoi  9475  rabssnn0fi  14021  fsuppmapnn0fiubex  14027  sumodd  16445  nosupbnd1  27843  nosupbnd2  27845  noinfbnd1  27858  noinfbnd2  27860  fprodex01  33109  ordtconnlem1  34258  esumrnmpt2  34402  ddemeas  34570  bnj1388  35365  bnj1398  35366  bnj1445  35376  bnj1449  35380  regsfromsetind  36938  finxpreclem6  37929  wl-nfnae1  38070  cdlemefs32sn1aw  41077  ss2iundf  44276  ax6e2ndeqALT  45530  uzwo4  45664  eliin2f  45713  stoweidlem55  46660  stoweidlem59  46664  etransclem32  46871  salexct  46939  sge0f1o  46987  incsmflem  47346  decsmflem  47371  r19.32  47723