Theorem nfnd 1860

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

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

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

This theorem depends on definitions:  df-bi 207  df-or 849  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfand  1899  nfan1  2208  hbnt  2301  nfexd  2335  cbvexdw  2344  cbvexd  2413  nfexd2  2451  nfned  3035  nfneld  3046  nfrexdw  3284  nfrexd  3345  cbvexeqsetf  3457  axpowndlem3  10522  axpowndlem4  10523  axregndlem2  10526  axregnd  10527  cbvex1v  35250  axnulg  35285  distel  36017  bj-cbvexdv  37048  bj-nfexd  37391  wl-issetft  37837