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
Assertion
Ref Expression
nfnd

Proof of Theorem nfnd
StepHypRef Expression
1 nfnd.1 . 2
2 nfnt 1848 . 2
31, 2syl 16 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4  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