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

Step	Hyp	Ref	Expression
1		pm2.01d.1	. 2 ⊢ (𝜑 → (𝜓 → ¬ 𝜓))
2		id 22	. 2 ⊢ (¬ 𝜓 → ¬ 𝜓)
3	1, 2	pm2.61d1 180	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  195  pm2.01da  798  swopo  5600  onssneli  6481  oalimcl  8560  rankcf  10772  prlem934  11028  supsrlem  11106  rpnnen1lem5  12965  rennim  15186  smu01lem  16426  opsrtoslem2  21617  cfinufil  23432  alexsub  23549  ostth3  27141  4cyclusnfrgr  29545  cvnref  31544  pconnconn  34222  untelirr  34677  dfon2lem4  34758  heiborlem10  36688  lindslinindsimp1  47138