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 181
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 171 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  187  pm2.01da  458  swopo  5043  onssneli  5835  oalimcl  7637  rankcf  9596  prlem934  9852  supsrlem  9929  rpnnen1lem5  11815  rpnnen1lem5OLD  11821  rennim  13973  smu01lem  15201  opsrtoslem2  19479  cfinufil  21726  alexsub  21843  ostth3  25321  4cyclusnfrgr  27149  cvnref  29134  pconnconn  31198  untelirr  31570  dfon2lem4  31675  heiborlem10  33599  lindslinindsimp1  42017
  Copyright terms: Public domain W3C validator