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 189
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 180 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  195  pm2.01da  798  swopo  5561  onssneli  6438  oalimcl  8512  rankcf  10720  prlem934  10976  supsrlem  11054  rpnnen1lem5  12913  rennim  15131  smu01lem  16372  opsrtoslem2  21479  cfinufil  23295  alexsub  23412  ostth3  27002  4cyclusnfrgr  29278  cvnref  31275  pconnconn  33865  untelirr  34319  dfon2lem4  34400  heiborlem10  36308  lindslinindsimp1  46612
  Copyright terms: Public domain W3C validator