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  5542  onssneli  6428  oalimcl  8485  rankcf  10690  prlem934  10946  supsrlem  11024  rpnnen1lem5  12900  rennim  15164  smu01lem  16414  opsrtoslem2  21979  cfinufil  23831  alexsub  23948  ostth3  27565  4cyclusnfrgr  30254  cvnref  32253  pconnconn  35206  untelirr  35683  dfon2lem4  35762  heiborlem10  37802  mod2addne  47352  pgnioedg1  48096  pgnioedg2  48097  pgnioedg3  48098  pgnioedg4  48099  pgnioedg5  48100  lindslinindsimp1  48446