Theorem nfn 1782

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

Syntax hints:  ¬ wn 3  Ⅎwnf 1705

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

This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1702  df-nf 1707

This theorem is referenced by:  nfanOLD  1831  nfnan  1832  nfor  1836  nfa1  2030  nfna1  2031  nfan1  2071  19.32  2104  nfex  2156  cbvexv1  2180  cbvex  2276  cbvex2  2284  nfnae  2322  axc14  2376  euor  2516  euor2  2518  nfne  2896  nfnel  2906  cbvrexf  3159  spcimegf  3278  spcegf  3280  cbvrexcsf  3552  nfdif  3714  rabsnifsb  4232  nfpo  5005  nffr  5053  rexxpf  5234  0neqopab  6652  boxcutc  7896  nfoi  8364  rabssnn0fi  12722  fsuppmapnn0fiubex  12729  sumodd  15030  spc2d  29153  ordtconnlem1  29744  esumrnmpt2  29903  ddemeas  30072  bnj1388  30801  bnj1398  30802  bnj1445  30812  bnj1449  30816  bj-cbvex2v  32372  finxpreclem6  32857  wl-nfnae1  32943  cdlemefs32sn1aw  35168  ss2iundf  37418  ax6e2ndeqALT  38636  uzwo4  38692  eliin2f  38758  stoweidlem55  39566  stoweidlem59  39570  etransclem32  39777  salexct  39846  sge0f1o  39893  incsmflem  40244  decsmflem  40268  r19.32  40458