MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfnd Structured version   Visualization version   GIF version

Theorem nfnd 1849
Description: Deduction associated with nfnt 1847. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypothesis
Ref Expression
nfnd.1 (𝜑 → Ⅎ𝑥𝜓)
Assertion
Ref Expression
nfnd (𝜑 → Ⅎ𝑥 ¬ 𝜓)

Proof of Theorem nfnd
StepHypRef Expression
1 nfnd.1 . 2 (𝜑 → Ⅎ𝑥𝜓)
2 nfnt 1847 . 2 (Ⅎ𝑥𝜓 → Ⅎ𝑥 ¬ 𝜓)
31, 2syl 17 1 (𝜑 → Ⅎ𝑥 ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wnf 1775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-or 842  df-ex 1772  df-nf 1776
This theorem is referenced by:  nfand  1889  nfan1  2190  hbnt  2293  nfexd  2339  cbvexdw  2350  cbvexd  2420  nfexd2  2460  nfned  3117  nfneld  3128  nfrexd  3304  nfrexdg  3305  vtoclgft  3551  axpowndlem3  10009  axpowndlem4  10010  axregndlem2  10013  axregnd  10014  distel  32945  bj-cbvexdv  34019  bj-nfexd  34322
  Copyright terms: Public domain W3C validator