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

Theorem nfnd 1850
Description: Deduction associated with nfnt 1848. (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 1848 . 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 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-ex 1597  df-nf 1600
This theorem is referenced by:  nfand  1872  nfexd  1899  cbvexd  1999  nfexd2  2047  nfned  2799  nfneld  2811  nfrexd  2926  axpowndlem2OLD  8970  axpowndlem3  8971  axpowndlem3OLD  8972  axpowndlem4  8973  axregndlem2  8976  axregnd  8977  axregndOLD  8978  distel  28813  wl-nfnbi  29556  bj-cbvexdv  33383
  Copyright terms: Public domain W3C validator