Theorem pm2.01d 190

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  196  pm2.01da  798  swopo  5572  onssneli  6470  oalimcl  8572  rankcf  10791  prlem934  11047  supsrlem  11125  rpnnen1lem5  12997  rennim  15258  smu01lem  16504  opsrtoslem2  22014  cfinufil  23866  alexsub  23983  ostth3  27601  4cyclusnfrgr  30273  cvnref  32272  pconnconn  35253  untelirr  35725  dfon2lem4  35804  heiborlem10  37844  lindslinindsimp1  48433