Theorem nfnd 1890

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

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

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

This proof depends on definitions:  df-bi 210  df-or 862  df-ex 1812  df-nf 1816

This theorem is used by:  nfand  1929  nfan1  2236  hbnt  2327  nfexd  2359  cbvexdw  2368  cbvexd  2437  nfexd2  2475  nfned  3059  nfneld  3070  nfrexdw  3308  nfrexd  3358  cbvexeqsetf  3465  axpowndlem3  10691  axpowndlem4  10692  axregndlem2  10695  axregnd  10696  cbvex1v  35754  axnulg  35873  distel  36661  bj-cbvexdv  37808  bj-nfexd  38166  wl-issetft  38623