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

Theorem pm2.01d 179
Description: Deduction based on reductio ad absurdum. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Mar-2013.)
Hypothesis
Ref Expression
pm2.01d.1 (𝜑 → (𝜓 → ¬ 𝜓))
Assertion
Ref Expression
pm2.01d (𝜑 → ¬ 𝜓)

Proof of Theorem pm2.01d
StepHypRef Expression
1 pm2.01d.1 . 2 (𝜑 → (𝜓 → ¬ 𝜓))
2 id 22 . 2 𝜓 → ¬ 𝜓)
31, 2pm2.61d1 169 1 (𝜑 → ¬ 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  pm2.65d  185  pm2.01da  456  swopo  4956  onssneli  5737  oalimcl  7501  rankcf  9452  prlem934  9708  supsrlem  9785  rpnnen1lem5  11647  rpnnen1lem5OLD  11653  rennim  13770  smu01lem  14988  opsrtoslem2  19249  cfinufil  21481  alexsub  21598  ostth3  25041  4cyclusnfrgra  26309  cvnref  28337  pconcon  30270  untelirr  30642  dfon2lem4  30738  heiborlem10  32589  4cyclusnfrgr  41461  lindslinindsimp1  42039
  Copyright terms: Public domain W3C validator