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

Theorem nexdv 1979
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 1953 . 2 (𝜑 → ∀𝑥𝜑)
2 nexdv.1 . 2 (𝜑 → ¬ 𝜓)
31, 2nexdh 1910 1 (𝜑 → ¬ ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wex 1823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953
This theorem depends on definitions:  df-bi 199  df-ex 1824
This theorem is referenced by:  sbc2or  3661  csbopab  5245  relimasn  5742  csbiota  6128  canthwdom  8773  cfsuc  9414  ssfin4  9467  konigthlem  9725  axunndlem1  9752  canthnum  9806  canthwe  9808  pwfseq  9821  tskuni  9940  ptcmplem4  22267  lgsquadlem3  25559  umgredgnlp  26496  dfrdg4  32647
  Copyright terms: Public domain W3C validator