Theorem pm2.01d 191

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 181	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  197  pm2.01da  804  swopo  5537  onssneli  6427  oalimcl  8485  elirrv  9502  rankcf  10691  prlem934  10947  supsrlem  11025  rpnnen1lem5  12922  rennim  15192  smu01lem  16445  opsrtoslem2  22032  cfinufil  23911  alexsub  24028  ostth3  27619  4cyclusnfrgr  30380  cvnref  32380  pconnconn  35459  untelirr  35936  dfon2lem4  36012  heiborlem10  38187  mod2addne  47833  pgnioedg1  48599  pgnioedg2  48600  pgnioedg3  48601  pgnioedg4  48602  pgnioedg5  48603  lindslinindsimp1  48948