Theorem nfnd 1859

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

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

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

This theorem depends on definitions:  df-bi 207  df-or 848  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfand  1898  nfan1  2207  hbnt  2300  nfexd  2334  cbvexdw  2343  cbvexd  2412  nfexd2  2450  nfned  3034  nfneld  3045  nfrexdw  3282  nfrexd  3343  cbvexeqsetf  3455  axpowndlem3  10510  axpowndlem4  10511  axregndlem2  10514  axregnd  10515  cbvex1v  35230  axnulg  35264  distel  35995  bj-cbvexdv  37001  bj-nfexd  37343  wl-issetft  37787