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

Theorem nexdv 1941
 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:   ,
Allowed substitution hint:   ()

Proof of Theorem nexdv
StepHypRef Expression
1 nfv 1629 . 2
2 nexdv.1 . 2
31, 2nexd 1787 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4  wex 1550 This theorem is referenced by:  sbc2or  3169  relimasn  5227  canthwdom  7547  cfsuc  8137  ssfin4  8190  konigthlem  8443  axunndlem1  8470  canthnum  8524  canthwe  8526  pwfseq  8539  tskuni  8658  ptcmplem4  18086  lgsquadlem3  21140  dfrdg4  25795 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761 This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554
 Copyright terms: Public domain W3C validator