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

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
StepHypRef Expression
1 nfv 1707 . 2
2 nexdv.1 . 2
31, 2nexd 1883 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator