Theorem nfnd 1885

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

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

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

This theorem depends on definitions:  df-bi 210  df-or 861  df-ex 1807  df-nf 1811

This theorem is referenced by:  nfand  1924  nfan1  2242  hbnt  2335  nfexd  2368  cbvexdw  2377  cbvexd  2446  nfexd2  2484  nfned  3068  nfneld  3079  nfrexdw  3317  nfrexd  3369  cbvexeqsetf  3478  axpowndlem3  10584  axpowndlem4  10585  axregndlem2  10588  axregnd  10589  cbvex1v  35407  axnulg  35481  distel  36192  bj-cbvexdv  37324  bj-nfexd  37668  wl-issetft  38125