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 171 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  458  swopo  5035  onssneli  5825  oalimcl  7625  rankcf  9584  prlem934  9840  supsrlem  9917  rpnnen1lem5  11803  rpnnen1lem5OLD  11809  rennim  13960  smu01lem  15188  opsrtoslem2  19466  cfinufil  21713  alexsub  21830  ostth3  25308  4cyclusnfrgr  27136  cvnref  29120  pconnconn  31187  untelirr  31559  dfon2lem4  31665  heiborlem10  33590  lindslinindsimp1  42011
  Copyright terms: Public domain W3C validator