MPE Home 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  |-  ( ph  ->  -.  ps )
Assertion
Ref Expression
nexdv  |-  ( ph  ->  -.  E. x ps )
Distinct variable group:    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem nexdv
StepHypRef Expression
1 nfv 1629 . 2  |-  F/ x ph
2 nexdv.1 . 2  |-  ( ph  ->  -.  ps )
31, 2nexd 1787 1  |-  ( ph  ->  -.  E. x ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   E.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