Theorem pm2.01d 192

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 23	. 2 ⊢ (¬ 𝜓 → ¬ 𝜓)
3	1, 2	pm2.61d1 182	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  199  pm2.01da  810  swopo  5578  onssneli  6476  oalimcl  8541  elirrv  9555  rankcf  10758  prlem934  11014  supsrlem  11092  rpnnen1lem5  13001  rennim  15286  smu01lem  16539  opsrtoslem2  22172  cfinufil  24050  alexsub  24167  ostth3  27764  4cyclusnfrgr  30580  cvnref  32580  pconnconn  35618  untelirr  36095  dfon2lem4  36171  heiborlem10  38354  mod2addne  47991  pgnioedg1  48757  pgnioedg2  48758  pgnioedg3  48759  pgnioedg4  48760  pgnioedg5  48761  lindslinindsimp1  49117