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  792  swopo  5180  onssneli  5980  oalimcl  7793  rankcf  9800  prlem934  10056  supsrlem  10133  rpnnen1lem5  12020  rpnnen1lem5OLD  12026  rennim  14186  smu01lem  15414  opsrtoslem2  19699  cfinufil  21951  alexsub  22068  ostth3  25547  4cyclusnfrgr  27471  cvnref  29484  pconnconn  31545  untelirr  31917  dfon2lem4  32021  heiborlem10  33944  lindslinindsimp1  42764
  Copyright terms: Public domain W3C validator