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

Theorem nfnd 1858
Description: Deduction associated with nfnt 1856. (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 1856 . 2 (Ⅎ𝑥𝜓 → Ⅎ𝑥 ¬ 𝜓)
31, 2syl 17 1 (𝜑 → Ⅎ𝑥 ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wnf 1783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-or 849  df-ex 1780  df-nf 1784
This theorem is referenced by:  nfand  1897  nfan1  2200  hbnt  2294  nfexd  2329  cbvexdw  2341  cbvexd  2413  nfexd2  2451  nfned  3044  nfneld  3055  nfrexdw  3310  nfrexd  3373  cbvexeqsetf  3495  axpowndlem3  10639  axpowndlem4  10640  axregndlem2  10643  axregnd  10644  cbvex1v  35088  axnulg  35106  distel  35804  bj-cbvexdv  36801  bj-nfexd  37139  wl-issetft  37583
  Copyright terms: Public domain W3C validator