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

Theorem nfnd 1838
Description: Deduction associated with nfnt 1836. (Contributed by Mario Carneiro, 24-Sep-2016.)
Hypothesis
Ref Expression
nfnd.1  |-  ( ph  ->  F/ x ps )
Assertion
Ref Expression
nfnd  |-  ( ph  ->  F/ x  -.  ps )

Proof of Theorem nfnd
StepHypRef Expression
1 nfnd.1 . 2  |-  ( ph  ->  F/ x ps )
2 nfnt 1836 . 2  |-  ( F/ x ps  ->  F/ x  -.  ps )
31, 2syl 16 1  |-  ( ph  ->  F/ x  -.  ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591
This theorem is referenced by:  nfand  1860  nfexd  1887  cbvexd  1983  nfexd2  2031  nfned  2780  nfneld  2792  nfrexd  2877  axpowndlem2OLD  8864  axpowndlem3  8865  axpowndlem3OLD  8866  axpowndlem4  8867  axregndlem2  8870  axregnd  8871  axregndOLD  8872  distel  27751  wl-nfnbi  28493  bj-cbvexdv  32537
  Copyright terms: Public domain W3C validator