Theorem nfnd 1858

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

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

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

This theorem depends on definitions:  df-bi 209  df-or 844  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfand  1898  nfan1  2200  hbnt  2302  nfexd  2348  cbvexdw  2359  cbvexd  2429  nfexd2  2468  nfned  3122  nfneld  3133  nfrexd  3309  nfrexdg  3310  vtoclgft  3555  axpowndlem3  10023  axpowndlem4  10024  axregndlem2  10027  axregnd  10028  distel  33050  bj-cbvexdv  34124  bj-nfexd  34432