Theorem nfn 1856

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

Syntax hints:  ¬ wn 3  Ⅎwnf 1781

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

This theorem depends on definitions:  df-bi 207  df-or 847  df-ex 1778  df-nf 1782

This theorem is referenced by:  nfnan  1899  nfor  1903  nfnaewOLD  2150  nfa1  2152  nfna1  2153  nfan1  2201  19.32  2234  nfex  2328  cbvexv1  2348  cbvex2v  2350  cbvex  2407  cbvex2  2420  nfnae  2442  axc14  2471  euor  2614  euor2  2616  nfne  3049  nfnel  3060  cbvrexfw  3311  cbvrexf  3369  ceqsex  3540  spcimegf  3563  spcegf  3605  spc2d  3615  cbvrexcsf  3967  nfdif  4152  nfdifOLD  4153  rabsnifsb  4747  0nelopabOLD  5587  nfpo  5613  nffr  5673  rexxpf  5872  boxcutc  8999  nfoi  9583  rabssnn0fi  14037  fsuppmapnn0fiubex  14043  sumodd  16436  nosupbnd1  27777  nosupbnd2  27779  noinfbnd1  27792  noinfbnd2  27794  fprodex01  32829  ordtconnlem1  33870  esumrnmpt2  34032  ddemeas  34200  bnj1388  35009  bnj1398  35010  bnj1445  35020  bnj1449  35024  finxpreclem6  37362  wl-nfnae1  37482  cdlemefs32sn1aw  40371  ss2iundf  43621  ax6e2ndeqALT  44902  uzwo4  44955  eliin2f  45006  stoweidlem55  45976  stoweidlem59  45980  etransclem32  46187  salexct  46255  sge0f1o  46303  incsmflem  46662  decsmflem  46687  r19.32  47013