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  796  swopo  5514  onssneli  6376  oalimcl  8391  rankcf  10533  prlem934  10789  supsrlem  10867  rpnnen1lem5  12721  rennim  14950  smu01lem  16192  opsrtoslem2  21263  cfinufil  23079  alexsub  23196  ostth3  26786  4cyclusnfrgr  28656  cvnref  30653  pconnconn  33193  untelirr  33649  dfon2lem4  33762  heiborlem10  35978  lindslinindsimp1  45798