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

Theorem nexdv 1889
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 1712 . 2  |-  F/ x ph
2 nexdv.1 . 2  |-  ( ph  ->  -.  ps )
31, 2nexd 1888 1  |-  ( ph  ->  -.  E. x ps )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4   E.wex 1617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-12 1859
This theorem depends on definitions:  df-bi 185  df-ex 1618  df-nf 1622
This theorem is referenced by:  sbc2or  3333  csbopab  4768  relimasn  5348  csbiota  5563  canthwdom  7997  cfsuc  8628  ssfin4  8681  konigthlem  8934  axunndlem1  8961  canthnum  9016  canthwe  9018  pwfseq  9031  tskuni  9150  ptcmplem4  20724  lgsquadlem3  23832  dfrdg4  29831  usgedgnlp  32801
  Copyright terms: Public domain W3C validator