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  3336  cbvexeqsetf  3445  axpowndlem3  10513  axpowndlem4  10514  axregndlem2  10517  axregnd  10518  cbvex1v  35232  axnulg  35267  distel  35999  bj-cbvexdv  37123  bj-nfexd  37466  wl-issetft  37921