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  2205  hbnt  2298  nfexd  2332  cbvexdw  2341  cbvexd  2410  nfexd2  2448  nfned  3031  nfneld  3042  nfrexdw  3279  nfrexd  3340  cbvexeqsetf  3452  axpowndlem3  10501  axpowndlem4  10502  axregndlem2  10505  axregnd  10506  cbvex1v  35158  axnulg  35191  distel  35917  bj-cbvexdv  36917  bj-nfexd  37255  wl-issetft  37699