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  5557  onssneli  6450  oalimcl  8524  rankcf  10730  prlem934  10986  supsrlem  11064  rpnnen1lem5  12940  rennim  15205  smu01lem  16455  opsrtoslem2  21963  cfinufil  23815  alexsub  23932  ostth3  27549  4cyclusnfrgr  30221  cvnref  32220  pconnconn  35218  untelirr  35695  dfon2lem4  35774  heiborlem10  37814  mod2addne  47365  pgnioedg1  48098  pgnioedg2  48099  pgnioedg3  48100  pgnioedg4  48101  pgnioedg5  48102  lindslinindsimp1  48446