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

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
StepHypRef Expression
1 nfnd.1 . 2 (𝜑 → Ⅎ𝑥𝜓)
2 nfnt 1860 . 2 (Ⅎ𝑥𝜓 → Ⅎ𝑥 ¬ 𝜓)
31, 2syl 17 1 (𝜑 → Ⅎ𝑥 ¬ 𝜓)
Colors of variables: wff setvar class
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  2407  nfexd2  2445  nfned  3047  nfneld  3058  nfrexdw  3296  nfrexd  3349  vtoclgft  3512  axpowndlem3  10542  axpowndlem4  10543  axregndlem2  10546  axregnd  10547  distel  34417  bj-cbvexdv  35294  bj-nfexd  35638  wl-issetft  36063
  Copyright terms: Public domain W3C validator