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  2239  hbnt  2331  nfexd  2364  cbvexdw  2373  cbvexd  2442  nfexd2  2480  nfned  3064  nfneld  3075  nfrexdw  3313  nfrexd  3364  cbvexeqsetf  3472  axpowndlem3  10595  axpowndlem4  10596  axregndlem2  10599  axregnd  10600  cbvex1v  35503  axnulg  35591  distel  36306  bj-cbvexdv  37468  bj-nfexd  37813  wl-issetft  38270