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

Theorem nexdv 1932
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 1906 . 2 (𝜑 → ∀𝑥𝜑)
2 nexdv.1 . 2 (𝜑 → ¬ 𝜓)
31, 2nexdh 1861 1 (𝜑 → ¬ ∃𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wex 1774
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906
This theorem depends on definitions:  df-bi 206  df-ex 1775
This theorem is referenced by:  sbc2or  3785  csbopab  5561  relimasn  6094  csbiota  6547  0mpo0  7508  1sdom2dom  9281  canthwdom  9622  cfsuc  10300  ssfin4  10353  konigthlem  10611  axunndlem1  10638  canthnum  10692  canthwe  10694  pwfseq  10707  tskuni  10826  ptcmplem4  24050  lgsquadlem3  27411  umgredgnlp  29083  iswspthsnon  29790  acycgr0v  34976  acycgr2v  34978  prclisacycgr  34979  dfrdg4  35775
  Copyright terms: Public domain W3C validator