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 193
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 183 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  199  pm2.01da  798  swopo  5452  onssneli  6272  oalimcl  8173  rankcf  10192  prlem934  10448  supsrlem  10526  rpnnen1lem5  12372  rennim  14593  smu01lem  15827  opsrtoslem2  20727  cfinufil  22536  alexsub  22653  ostth3  26225  4cyclusnfrgr  28080  cvnref  30077  pconnconn  32586  untelirr  33042  dfon2lem4  33139  heiborlem10  35251  lindslinindsimp1  44853
  Copyright terms: Public domain W3C validator