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  1932  nfan1  2240  hbnt  2331  nfexd  2363  cbvexdw  2372  cbvexd  2440  nfexd2  2478  nfned  3063  nfneld  3074  nfrexdw  3312  nfrexd  3362  cbvexeqsetf  3469  axpowndlem3  10723  axpowndlem4  10724  axregndlem2  10727  axregnd  10728  cbvex1v  35815  axnulg  35954  distel  36780  bj-cbvexdv  37927  bj-nfexd  38328  wl-issetft  38782