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  2325  cbvexv1  2344  cbvex2v  2346  cbvex  2404  cbvex2  2417  nfnae  2439  axc14  2468  euor  2611  euor2  2613  nfne  3034  nfnel  3045  cbvrexfw  3289  cbvrexf  3345  ceqsex  3514  spcimegf  3535  spcegf  3576  spc2d  3586  cbvrexcsf  3922  nfdif  4109  nfdifOLD  4110  rabsnifsb  4703  nfpo  5572  nffr  5632  rexxpf  5832  boxcutc  8960  nfoi  9533  rabssnn0fi  14009  fsuppmapnn0fiubex  14015  sumodd  16412  nosupbnd1  27683  nosupbnd2  27685  noinfbnd1  27698  noinfbnd2  27700  fprodex01  32809  ordtconnlem1  33960  esumrnmpt2  34104  ddemeas  34272  bnj1388  35069  bnj1398  35070  bnj1445  35080  bnj1449  35084  finxpreclem6  37419  wl-nfnae1  37551  cdlemefs32sn1aw  40438  ss2iundf  43650  ax6e2ndeqALT  44922  uzwo4  45044  eliin2f  45095  stoweidlem55  46051  stoweidlem59  46055  etransclem32  46262  salexct  46330  sge0f1o  46378  incsmflem  46737  decsmflem  46762  r19.32  47094