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 207  df-or 847  df-ex 1778  df-nf 1782

This theorem is referenced by:  nfand  1896  nfan1  2201  hbnt  2298  nfexd  2333  cbvexdw  2345  cbvexd  2416  nfexd2  2454  nfned  3050  nfneld  3061  nfrexdw  3316  nfrexd  3381  cbvexeqsetf  3503  axpowndlem3  10668  axpowndlem4  10669  axregndlem2  10672  axregnd  10673  cbvex1v  35050  axnulg  35068  distel  35767  bj-cbvexdv  36766  bj-nfexd  37104  wl-issetft  37536