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  5555  onssneli  6431  oalimcl  8500  rankcf  10672  prlem934  10928  supsrlem  11006  rpnnen1lem5  12861  rennim  15084  smu01lem  16325  opsrtoslem2  21415  cfinufil  23231  alexsub  23348  ostth3  26938  4cyclusnfrgr  29065  cvnref  31062  pconnconn  33629  untelirr  34085  dfon2lem4  34171  heiborlem10  36211  lindslinindsimp1  46433
  Copyright terms: Public domain W3C validator