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 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 210  df-or 845  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfand  1898  nfan1  2198  hbnt  2298  nfexd  2337  cbvexdw  2348  cbvexd  2418  nfexd2  2457  nfned  3088  nfneld  3099  nfrexd  3266  nfrexdg  3267  vtoclgft  3501  axpowndlem3  10010  axpowndlem4  10011  axregndlem2  10014  axregnd  10015  distel  33161  bj-cbvexdv  34237  bj-nfexd  34553