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  2334  cbvexdw  2343  cbvexd  2412  nfexd2  2450  nfned  3034  nfneld  3045  nfrexdw  3283  nfrexd  3335  cbvexeqsetf  3444  axpowndlem3  10522  axpowndlem4  10523  axregndlem2  10526  axregnd  10527  cbvex1v  35216  axnulg  35251  distel  35983  bj-cbvexdv  37107  bj-nfexd  37450  wl-issetft  37907