Theorem nfnd 1862

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

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

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

This theorem depends on definitions:  df-bi 206  df-or 844  df-ex 1784  df-nf 1788

This theorem is referenced by:  nfand  1901  nfan1  2196  hbnt  2294  nfexd  2327  cbvexdw  2338  cbvexd  2408  nfexd2  2446  nfned  3045  nfneld  3056  nfrexd  3235  nfrexdg  3236  vtoclgft  3482  axpowndlem3  10286  axpowndlem4  10287  axregndlem2  10290  axregnd  10291  distel  33685  bj-cbvexdv  34909  bj-nfexd  35236