Theorem nfn 1856

Description: Inference associated with nfnt 1855. (Contributed by Mario Carneiro, 11-Aug-2016.) df-nf 1783 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 1782

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

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1779  df-nf 1783

This theorem is referenced by:  nfnan  1899  nfor  1903  nfa1  2150  nfna1  2151  nfan1  2199  19.32  2232  nfex  2323  cbvexv1  2343  cbvex2v  2345  cbvex  2403  cbvex2  2416  nfnae  2438  axc14  2467  euor  2610  euor2  2612  nfne  3042  nfnel  3053  cbvrexfw  3304  cbvrexf  3360  ceqsex  3529  spcimegf  3550  spcegf  3591  spc2d  3601  cbvrexcsf  3941  nfdif  4128  nfdifOLD  4129  rabsnifsb  4721  nfpo  5597  nffr  5657  rexxpf  5857  boxcutc  8982  nfoi  9555  rabssnn0fi  14028  fsuppmapnn0fiubex  14034  sumodd  16426  nosupbnd1  27760  nosupbnd2  27762  noinfbnd1  27775  noinfbnd2  27777  fprodex01  32828  ordtconnlem1  33924  esumrnmpt2  34070  ddemeas  34238  bnj1388  35048  bnj1398  35049  bnj1445  35059  bnj1449  35063  finxpreclem6  37398  wl-nfnae1  37530  cdlemefs32sn1aw  40417  ss2iundf  43677  ax6e2ndeqALT  44956  uzwo4  45063  eliin2f  45114  stoweidlem55  46075  stoweidlem59  46079  etransclem32  46286  salexct  46354  sge0f1o  46402  incsmflem  46761  decsmflem  46786  r19.32  47115