Theorem pm2.01d 191

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

Step	Hyp	Ref	Expression
1		pm2.01d.1	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜓))
2		id 22	. 2 ⊢ (¬ 𝜓 → ¬ 𝜓)
3	1, 2	pm2.61d1 181	1 ⊢ (𝜑 → ¬ 𝜓)

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  197  pm2.01da  795  swopo  5372  onssneli  6175  oalimcl  8036  rankcf  10045  prlem934  10301  supsrlem  10379  rpnnen1lem5  12230  rennim  14432  smu01lem  15667  opsrtoslem2  19952  cfinufil  22220  alexsub  22337  ostth3  25896  4cyclusnfrgr  27763  cvnref  29759  pconnconn  32086  untelirr  32542  dfon2lem4  32639  heiborlem10  34630  lindslinindsimp1  43992