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  797  swopo  5597  onssneli  6484  oalimcl  8582  rankcf  10811  prlem934  11067  supsrlem  11145  rpnnen1lem5  13011  rennim  15239  smu01lem  16480  opsrtoslem2  22065  cfinufil  23920  alexsub  24037  ostth3  27664  4cyclusnfrgr  30222  cvnref  32221  pconnconn  35072  untelirr  35543  dfon2lem4  35623  heiborlem10  37534  lindslinindsimp1  47876
  Copyright terms: Public domain W3C validator