Theorem nfnd 1877

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

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

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

This theorem depends on definitions:  df-bi 209  df-or 859  df-ex 1799  df-nf 1803

This theorem is referenced by:  nfand  1916  nfan1  2234  hbnt  2327  nfexd  2360  cbvexdw  2369  cbvexd  2438  nfexd2  2476  nfned  3058  nfneld  3069  nfrexdw  3307  nfrexd  3359  cbvexeqsetf  3468  axpowndlem3  10551  axpowndlem4  10552  axregndlem2  10555  axregnd  10556  cbvex1v  35330  axnulg  35402  distel  36112  bj-cbvexdv  37246  bj-nfexd  37589  wl-issetft  38046