Theorem nexdv 1884

Description: Deduction for generalization rule for negated wff. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
nexdv.1

Assertion

Ref	Expression
nexdv

Distinct variable group:   ,

Proof of Theorem nexdv

Step	Hyp	Ref	Expression
1		nfv 1707	. 2
2		nexdv.1	. 2
3	1, 2	nexd 1883	1

Syntax hints:  -.wn 3  ->wi 4  E.wex 1612

This theorem is referenced by:  sbc2or  3336  csbopab  4784  relimasn  5365  csbiota  5585  canthwdom  8026  cfsuc  8658  ssfin4  8711  konigthlem  8964  axunndlem1  8991  canthnum  9048  canthwe  9050  pwfseq  9063  tskuni  9182  ptcmplem4  20555  lgsquadlem3  23631  dfrdg4  29600  usgedgnlp  32410

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-12 1854

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