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 191
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 181 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  197  pm2.01da  795  swopo  5372  onssneli  6175  oalimcl  8036  rankcf  10045  prlem934  10301  supsrlem  10379  rpnnen1lem5  12230  rennim  14432  smu01lem  15667  opsrtoslem2  19952  cfinufil  22220  alexsub  22337  ostth3  25896  4cyclusnfrgr  27763  cvnref  29759  pconnconn  32086  untelirr  32542  dfon2lem4  32639  heiborlem10  34630  lindslinindsimp1  43992
  Copyright terms: Public domain W3C validator