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

Theorem nexdv 1820
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 1674 . 2  |-  F/ x ph
2 nexdv.1 . 2  |-  ( ph  ->  -.  ps )
31, 2nexd 1819 1  |-  ( ph  ->  -.  E. x ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4   E.wex 1587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-ex 1588  df-nf 1591
This theorem is referenced by:  sbc2or  3293  csbopab  4718  relimasn  5290  csbiota  5508  canthwdom  7895  cfsuc  8527  ssfin4  8580  konigthlem  8833  axunndlem1  8860  canthnum  8917  canthwe  8919  pwfseq  8932  tskuni  9051  ptcmplem4  19743  lgsquadlem3  22811  dfrdg4  28115
  Copyright terms: Public domain W3C validator