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

Theorem nexdv 1940
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 1914 . 2 (𝜑 → ∀𝑥𝜑)
2 nexdv.1 . 2 (𝜑 → ¬ 𝜓)
31, 2nexdh 1869 1 (𝜑 → ¬ ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-ex 1783
This theorem is referenced by:  sbc2or  3753  csbopab  5517  relimasn  6041  csbiota  6494  0mpo0  7445  1sdom2dom  9198  canthwdom  9522  cfsuc  10200  ssfin4  10253  konigthlem  10511  axunndlem1  10538  canthnum  10592  canthwe  10594  pwfseq  10607  tskuni  10726  ptcmplem4  23422  lgsquadlem3  26746  umgredgnlp  28140  iswspthsnon  28843  acycgr0v  33782  acycgr2v  33784  prclisacycgr  33785  dfrdg4  34565
  Copyright terms: Public domain W3C validator