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

Theorem nfnd 1859
Description: Deduction associated with nfnt 1857. (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 1857 . 2 (Ⅎ𝑥𝜓 → Ⅎ𝑥 ¬ 𝜓)
31, 2syl 17 1 (𝜑 → Ⅎ𝑥 ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wnf 1785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811
This theorem depends on definitions:  df-bi 210  df-or 845  df-ex 1782  df-nf 1786
This theorem is referenced by:  nfand  1899  nfan1  2202  hbnt  2304  nfexd  2350  cbvexdw  2361  cbvexd  2431  nfexd2  2470  nfned  3114  nfneld  3125  nfrexd  3299  nfrexdg  3300  vtoclgft  3538  axpowndlem3  10006  axpowndlem4  10007  axregndlem2  10010  axregnd  10011  distel  33066  bj-cbvexdv  34141  bj-nfexd  34458
  Copyright terms: Public domain W3C validator