Theorem nfnd 1858

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

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

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

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

This theorem is referenced by:  nfand  1897  nfan1  2201  hbnt  2294  nfexd  2328  cbvexdw  2337  cbvexd  2406  nfexd2  2444  nfned  3027  nfneld  3038  nfrexdw  3284  nfrexd  3347  cbvexeqsetf  3462  axpowndlem3  10552  axpowndlem4  10553  axregndlem2  10556  axregnd  10557  cbvex1v  35064  axnulg  35082  distel  35791  bj-cbvexdv  36788  bj-nfexd  37126  wl-issetft  37570