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

Theorem pm2.01d 180
 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 170 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  186  pm2.01da  457  swopo  4969  onssneli  5754  oalimcl  7527  rankcf  9478  prlem934  9734  supsrlem  9811  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  rennim  13827  smu01lem  15045  opsrtoslem2  19306  cfinufil  21542  alexsub  21659  ostth3  25127  4cyclusnfrgra  26546  cvnref  28534  pconcon  30467  untelirr  30839  dfon2lem4  30935  heiborlem10  32789  4cyclusnfrgr  41462  lindslinindsimp1  42040
 Copyright terms: Public domain W3C validator