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

Theorem nexdv 1937
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 1911 . 2 (𝜑 → ∀𝑥𝜑)
2 nexdv.1 . 2 (𝜑 → ¬ 𝜓)
31, 2nexdh 1866 1 (𝜑 → ¬ ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wex 1781
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911
This theorem depends on definitions:  df-bi 210  df-ex 1782
This theorem is referenced by:  sbc2or  3732  csbopab  5410  relimasn  5923  csbiota  6321  0mpo0  7220  canthwdom  9031  cfsuc  9672  ssfin4  9725  konigthlem  9983  axunndlem1  10010  canthnum  10064  canthwe  10066  pwfseq  10079  tskuni  10198  ptcmplem4  22663  lgsquadlem3  25969  umgredgnlp  26943  iswspthsnon  27645  acycgr0v  32503  acycgr2v  32505  prclisacycgr  32506  dfrdg4  33520
  Copyright terms: Public domain W3C validator