Theorem nfnd 1859

Description: Deduction associated with nfnt 1857. (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 1857	. 2 ⊢ (Ⅎ𝑥𝜓 → Ⅎ𝑥 ¬ 𝜓)
3	1, 2	syl 17	1 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜓)

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

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

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfand  1898  nfan1  2203  hbnt  2296  nfexd  2330  cbvexdw  2339  cbvexd  2408  nfexd2  2446  nfned  3030  nfneld  3041  nfrexdw  3278  nfrexd  3339  cbvexeqsetf  3451  axpowndlem3  10485  axpowndlem4  10486  axregndlem2  10489  axregnd  10490  cbvex1v  35078  axnulg  35111  distel  35837  bj-cbvexdv  36834  bj-nfexd  37172  wl-issetft  37616