Theorem nfnd 1888

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

Syntax hints:  ¬ wn 3   → wi 4  Ⅎwnf 1813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839

This theorem depends on definitions:  df-bi 210  df-or 861  df-ex 1810  df-nf 1814

This theorem is referenced by:  nfand  1927  nfan1  2236  hbnt  2329  nfexd  2362  cbvexdw  2371  cbvexd  2440  nfexd2  2478  nfned  3062  nfneld  3073  nfrexdw  3311  nfrexd  3362  cbvexeqsetf  3470  axpowndlem3  10579  axpowndlem4  10580  axregndlem2  10583  axregnd  10584  cbvex1v  35462  axnulg  35558  distel  36293  bj-cbvexdv  37435  bj-nfexd  37780  wl-issetft  38237