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

Theorem nexdv 2001
Description: Deduction for generalization rule for negated wff. (Contributed by NM, 5-Aug-1993.) Reduce dependencies on axioms. (Revised by Wolf Lammen, 13-Jul-2020.) (Proof shortened by Wolf Lammen, 10-Oct-2021.)
Hypothesis
Ref Expression
nexdv.1 (𝜑 → ¬ 𝜓)
Assertion
Ref Expression
nexdv (𝜑 → ¬ ∃𝑥𝜓)
Distinct variable group:   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem nexdv
StepHypRef Expression
1 ax-5 1976 . 2 (𝜑 → ∀𝑥𝜑)
2 nexdv.1 . 2 (𝜑 → ¬ 𝜓)
31, 2nexdh 1929 1 (𝜑 → ¬ ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wex 1841
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976
This theorem depends on definitions:  df-bi 197  df-ex 1842
This theorem is referenced by:  sbc2or  3573  csbopab  5146  relimasn  5634  csbiota  6030  canthwdom  8637  cfsuc  9242  ssfin4  9295  konigthlem  9553  axunndlem1  9580  canthnum  9634  canthwe  9636  pwfseq  9649  tskuni  9768  ptcmplem4  22031  lgsquadlem3  25277  umgredgnlp  26212  dfrdg4  32335
  Copyright terms: Public domain W3C validator