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 172 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  824  swopo  5249  onssneli  6053  oalimcl  7880  rankcf  9887  prlem934  10143  supsrlem  10220  rpnnen1lem5  12040  rennim  14205  smu01lem  15429  opsrtoslem2  19696  cfinufil  21949  alexsub  22066  ostth3  25547  4cyclusnfrgr  27473  cvnref  29484  pconnconn  31541  untelirr  31912  dfon2lem4  32016  heiborlem10  33932  lindslinindsimp1  42815
  Copyright terms: Public domain W3C validator