Theorem nfn 1768

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

Syntax hints:  ¬ wn 3  Ⅎwnf 1699

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

This theorem depends on definitions:  df-bi 196  df-or 384  df-ex 1696  df-nf 1701

This theorem is referenced by:  nfanOLD  1817  nfnan  1818  nfor  1822  nfa1  2015  nfna1  2016  nfan1  2056  19.32  2088  nfex  2140  cbvexv1  2164  cbvex  2260  cbvex2  2268  nfnae  2306  axc14  2360  euor  2500  euor2  2502  nfne  2882  nfnel  2890  cbvrexf  3142  spcimegf  3260  spcegf  3262  cbvrexcsf  3532  nfdif  3693  rabsnifsb  4201  nfpo  4964  nffr  5012  rexxpf  5191  0neqopab  6596  boxcutc  7837  nfoi  8302  rabssnn0fi  12647  fsuppmapnn0fiubex  12654  sumodd  14949  spc2d  28697  ordtconlem1  29298  esumrnmpt2  29457  ddemeas  29626  bnj1388  30355  bnj1398  30356  bnj1445  30366  bnj1449  30370  bj-cbvex2v  31925  finxpreclem6  32409  wl-nfnae1  32495  cdlemefs32sn1aw  34720  ss2iundf  36970  ax6e2ndeqALT  38189  uzwo4  38246  eliin2f  38316  stoweidlem55  38948  stoweidlem59  38952  etransclem32  39159  salexct  39228  sge0f1o  39275  incsmflem  39628  decsmflem  39652  r19.32  39816