Theorem nfnd 1891

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-or 862  df-ex 1813  df-nf 1817

This theorem is used by:  nfand  1930  nfan1  2236  hbnt  2327  nfexd  2359  cbvexdw  2368  cbvexd  2437  nfexd2  2475  nfned  3059  nfneld  3070  nfrexdw  3308  nfrexd  3358  cbvexeqsetf  3465  axpowndlem3  10608  axpowndlem4  10609  axregndlem2  10612  axregnd  10613  cbvex1v  35583  axnulg  35671  distel  36380  bj-cbvexdv  37543  bj-nfexd  37888  wl-issetft  38345