Theorem pm2.01d 181

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 172	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  187  pm2.01da  824  swopo  5249  onssneli  6053  oalimcl  7880  rankcf  9887  prlem934  10143  supsrlem  10220  rpnnen1lem5  12040  rennim  14205  smu01lem  15429  opsrtoslem2  19696  cfinufil  21949  alexsub  22066  ostth3  25547  4cyclusnfrgr  27473  cvnref  29484  pconnconn  31541  untelirr  31912  dfon2lem4  32016  heiborlem10  33932  lindslinindsimp1  42815