Theorem nfnd 1902

Description: Deduction associated with nfnt 1900. (Contributed by Mario Carneiro, 24-Sep-2016.)

Hypothesis

Ref	Expression
nfnd.1

Assertion

Ref	Expression
nfnd

Proof of Theorem nfnd

Step	Hyp	Ref	Expression
1		nfnd.1	. 2
2		nfnt 1900	. 2
3	1, 2	syl 16	1

Syntax hints:  -.wn 3  ->wi 4  F/wnf 1616

This theorem is referenced by:  nfand  1925  nfexd  1952  cbvexd  2026  nfexd2  2074  nfned  2789  nfneld  2801  nfrexd  2919  axpowndlem2OLD  8995  axpowndlem3  8996  axpowndlem3OLD  8997  axpowndlem4  8998  axregndlem2  9001  axregnd  9002  axregndOLD  9003  distel  29236  bj-cbvexdv  34301

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854

This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617