Theorem pm2.01d 180

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 170	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  186  pm2.01da  457  swopo  4969  onssneli  5754  oalimcl  7527  rankcf  9478  prlem934  9734  supsrlem  9811  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  rennim  13827  smu01lem  15045  opsrtoslem2  19306  cfinufil  21542  alexsub  21659  ostth3  25127  4cyclusnfrgra  26546  cvnref  28534  pconcon  30467  untelirr  30839  dfon2lem4  30935  heiborlem10  32789  4cyclusnfrgr  41462  lindslinindsimp1  42040