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  2237  hbnt  2328  nfexd  2360  cbvexdw  2369  cbvexd  2438  nfexd2  2476  nfned  3060  nfneld  3071  nfrexdw  3309  nfrexd  3359  cbvexeqsetf  3466  axpowndlem3  10677  axpowndlem4  10678  axregndlem2  10681  axregnd  10682  cbvex1v  35697  axnulg  35796  distel  36545  bj-cbvexdv  37692  bj-nfexd  38037  wl-issetft  38494