Theorem nfnd 1861

Description: Deduction associated with nfnt 1859. (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 1859	. 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 206  df-or 846  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfand  1900  nfan1  2193  hbnt  2290  nfexd  2322  cbvexdw  2335  cbvexd  2407  nfexd2  2445  nfned  3044  nfneld  3055  nfrexdw  3307  nfrexd  3369  vtoclgft  3540  axpowndlem3  10590  axpowndlem4  10591  axregndlem2  10594  axregnd  10595  distel  34763  bj-cbvexdv  35666  bj-nfexd  36007  wl-issetft  36432