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 1786

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

This theorem depends on definitions:  df-bi 206  df-or 847  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfand  1901  nfan1  2194  hbnt  2291  nfexd  2323  cbvexdw  2336  cbvexd  2408  nfexd2  2446  nfned  3045  nfneld  3056  nfrexdw  3308  nfrexd  3370  vtoclgft  3541  axpowndlem3  10594  axpowndlem4  10595  axregndlem2  10598  axregnd  10599  distel  34775  bj-cbvexdv  35678  bj-nfexd  36019  wl-issetft  36444