Theorem nfnd 1857

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

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

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

This theorem depends on definitions:  df-bi 206  df-or 844  df-ex 1778  df-nf 1782

This theorem is referenced by:  nfand  1896  nfan1  2188  hbnt  2286  nfexd  2318  cbvexdw  2331  cbvexd  2403  nfexd2  2441  nfned  3041  nfneld  3052  nfrexd  3268  nfrexdg  3269  vtoclgft  3494  axpowndlem3  10383  axpowndlem4  10384  axregndlem2  10387  axregnd  10388  distel  33807  bj-cbvexdv  35010  bj-nfexd  35337