Theorem nfnd 1885

Description: Deduction associated with nfnt 1883. (Contributed by Mario Carneiro, 24-Sep-2016.)

Hypothesis

Ref	Expression
nfnd.1	⊢ (𝜑 → Ⅎ𝑥𝜓)

Assertion

Ref	Expression
nfnd	⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)

Proof of Theorem nfnd

Step	Hyp	Ref	Expression
1		nfnd.1	. 2 ⊢ (𝜑 → Ⅎ𝑥𝜓)
2		nfnt 1883	. 2 ⊢ (Ⅎ𝑥𝜓 → Ⅎ𝑥 ¬ 𝜓)
3	1, 2	syl 18	1 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4  Ⅎwnf 1810

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

This theorem depends on definitions:  df-bi 210  df-or 861  df-ex 1807  df-nf 1811

This theorem is referenced by:  nfand  1924  nfan1  2242  hbnt  2335  nfexd  2368  cbvexdw  2377  cbvexd  2446  nfexd2  2484  nfned  3068  nfneld  3079  nfrexdw  3317  nfrexd  3369  cbvexeqsetf  3478  axpowndlem3  10580  axpowndlem4  10581  axregndlem2  10584  axregnd  10585  cbvex1v  35403  axnulg  35477  distel  36188  bj-cbvexdv  37320  bj-nfexd  37663  wl-issetft  38120