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  5540  onssneli  6431  oalimcl  8484  rankcf  10679  prlem934  10935  supsrlem  11013  rpnnen1lem5  12885  rennim  15153  smu01lem  16403  opsrtoslem2  22002  cfinufil  23863  alexsub  23980  ostth3  27596  4cyclusnfrgr  30293  cvnref  32292  pconnconn  35347  untelirr  35824  dfon2lem4  35900  heiborlem10  37933  mod2addne  47526  pgnioedg1  48270  pgnioedg2  48271  pgnioedg3  48272  pgnioedg4  48273  pgnioedg5  48274  lindslinindsimp1  48619