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

Theorem nexdv 1857
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 1605 . 2  |-  F/ x ph
2 nexdv.1 . 2  |-  ( ph  ->  -.  ps )
31, 2nexd 1751 1  |-  ( ph  ->  -.  E. x ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   E.wex 1528
This theorem is referenced by:  sbc2or  2999  relimasn  5036  canthwdom  7293  cfsuc  7883  ssfin4  7936  konigthlem  8190  axunndlem1  8217  canthnum  8271  canthwe  8273  pwfseq  8286  tskuni  8405  ptcmplem4  17749  lgsquadlem3  20595  dfrdg4  24488
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator