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

Theorem nexdv 1869
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 1609 . 2  |-  F/ x ph
2 nexdv.1 . 2  |-  ( ph  ->  -.  ps )
31, 2nexd 1763 1  |-  ( ph  ->  -.  E. x ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   E.wex 1531
This theorem is referenced by:  sbc2or  3012  relimasn  5052  canthwdom  7309  cfsuc  7899  ssfin4  7952  konigthlem  8206  axunndlem1  8233  canthnum  8287  canthwe  8289  pwfseq  8302  tskuni  8421  ptcmplem4  17765  lgsquadlem3  20611  dfrdg4  24560
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator