Theorem nfnd 1865

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

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

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

This theorem depends on definitions:  df-bi 208  df-or 854  df-ex 1787  df-nf 1791

This theorem is referenced by:  nfand  1904  nfan1  2212  hbnt  2305  nfexd  2338  cbvexdw  2347  cbvexd  2416  nfexd2  2454  nfned  3036  nfneld  3047  nfrexdw  3285  nfrexd  3337  cbvexeqsetf  3446  axpowndlem3  10513  axpowndlem4  10514  axregndlem2  10517  axregnd  10518  cbvex1v  35256  axnulg  35326  distel  36029  bj-cbvexdv  37153  bj-nfexd  37496  wl-issetft  37953