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  5530  onssneli  6418  oalimcl  8470  rankcf  10663  prlem934  10919  supsrlem  10997  rpnnen1lem5  12874  rennim  15141  smu01lem  16391  opsrtoslem2  21986  cfinufil  23838  alexsub  23955  ostth3  27571  4cyclusnfrgr  30264  cvnref  32263  pconnconn  35267  untelirr  35744  dfon2lem4  35820  heiborlem10  37860  mod2addne  47395  pgnioedg1  48139  pgnioedg2  48140  pgnioedg3  48141  pgnioedg4  48142  pgnioedg5  48143  lindslinindsimp1  48489