Theorem pm2.01d 192

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 182	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  198  pm2.01da  797  swopo  5487  onssneli  6303  oalimcl  8189  rankcf  10202  prlem934  10458  supsrlem  10536  rpnnen1lem5  12383  rennim  14601  smu01lem  15837  opsrtoslem2  20268  cfinufil  22539  alexsub  22656  ostth3  26217  4cyclusnfrgr  28074  cvnref  30071  pconnconn  32482  untelirr  32938  dfon2lem4  33035  heiborlem10  35102  lindslinindsimp1  44519