Theorem nfnd 1855

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

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

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

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1776  df-nf 1780

This theorem is referenced by:  nfand  1894  nfan1  2197  hbnt  2292  nfexd  2327  cbvexdw  2339  cbvexd  2410  nfexd2  2448  nfned  3041  nfneld  3052  nfrexdw  3307  nfrexd  3370  cbvexeqsetf  3492  axpowndlem3  10636  axpowndlem4  10637  axregndlem2  10640  axregnd  10641  cbvex1v  35066  axnulg  35084  distel  35784  bj-cbvexdv  36782  bj-nfexd  37120  wl-issetft  37562