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

Theorem nexdv 1904
 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 1879 . 2 (𝜑 → ∀𝑥𝜑)
2 nexdv.1 . 2 (𝜑 → ¬ 𝜓)
31, 2nexdh 1832 1 (𝜑 → ¬ ∃𝑥𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4  ∃wex 1744 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879 This theorem depends on definitions:  df-bi 197  df-ex 1745 This theorem is referenced by:  sbc2or  3477  csbopab  5037  relimasn  5523  csbiota  5919  canthwdom  8525  cfsuc  9117  ssfin4  9170  konigthlem  9428  axunndlem1  9455  canthnum  9509  canthwe  9511  pwfseq  9524  tskuni  9643  ptcmplem4  21906  lgsquadlem3  25152  umgredgnlp  26087  dfrdg4  32183
 Copyright terms: Public domain W3C validator