Theorem nfn 1933

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

Syntax hints:  ¬ wn 3  Ⅎwnf 1857

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

This theorem depends on definitions:  df-bi 197  df-or 384  df-ex 1854  df-nf 1859

This theorem is referenced by:  nfanOLD  1978  nfnan  1979  nfor  1983  nfa1  2177  nfna1  2178  nfan1  2215  19.32  2248  nfex  2301  cbvexv1  2321  cbvex  2417  cbvex2  2425  nfnae  2460  axc14  2509  euor  2650  euor2  2652  nfne  3032  nfnel  3042  cbvrexf  3305  spcimegf  3427  spcegf  3429  cbvrexcsf  3707  nfdif  3874  rabsnifsb  4401  nfpo  5192  nffr  5240  rexxpf  5425  0neqopab  6863  boxcutc  8117  nfoi  8584  rabssnn0fi  12979  fsuppmapnn0fiubex  12986  sumodd  15313  spc2d  29622  fprodex01  29880  ordtconnlem1  30279  esumrnmpt2  30439  ddemeas  30608  bnj1388  31408  bnj1398  31409  bnj1445  31419  bnj1449  31423  nosupbnd1  32166  nosupbnd2  32168  bj-cbvex2v  33044  finxpreclem6  33544  wl-nfnae1  33629  cdlemefs32sn1aw  36204  ss2iundf  38453  ax6e2ndeqALT  39666  uzwo4  39720  eliin2f  39786  stoweidlem55  40775  stoweidlem59  40779  etransclem32  40986  salexct  41055  sge0f1o  41102  incsmflem  41456  decsmflem  41480  r19.32  41673