Theorem nfn 1890

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

This proof depends on syntax axioms:  ¬ wn 3  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-or 862  df-ex 1813  df-nf 1817

This theorem is used by:  nfnan  1935  nfor  1939  nfa1  2191  nfna1  2192  nfan1  2240  19.32  2273  nfex  2358  cbvexv1  2375  cbvex2v  2377  cbvex  2431  cbvex2  2444  nfnae  2466  axc14  2495  euor  2639  euor2  2641  nfne  3062  nfnel  3073  cbvrexfw  3307  cbvrexf  3350  ceqsex  3501  spcimegf  3518  spcegf  3550  spc2d  3560  cbvrexcsf  3894  nfdif  4069  rabsnifsb  4685  nfpo  5572  nffr  5631  rexxpf  5835  boxcutc  9007  nfoi  9545  rabssnn0fi  14169  fsuppmapnn0fiubex  14175  sumodd  16602  nosupbnd1  28128  nosupbnd2  28130  noinfbnd1  28143  noinfbnd2  28145  fprodex01  33512  ordtconnlem1  34667  esumrnmpt2  34811  ddemeas  34980  bnj1388  35774  bnj1398  35775  bnj1445  35785  bnj1449  35789  rmo6  35821  regsfromsetind  37542  finxpreclem6  38587  wl-nfnae1  38728  cdlemefs32sn1aw  41737  ss2iundf  44920  ax6e2ndeqALT  46173  uzwo4  46344  eliin2f  46392  stoweidlem55  47338  stoweidlem59  47342  etransclem32  47549  salexct  47617  sge0f1o  47665  incsmflem  48024  decsmflem  48049  r19.32  48442